#include <Grid.defs.hh>

Collaboration diagram for Parma_Polyhedra_Library::Grid:

Classes
class	Status
	A conjunctive assertion about a grid. More...
Public Types
typedef Coefficient	coefficient_type
	The numeric type of coefficients.
Public Member Functions
	Grid (dimension_type num_dimensions=0, Degenerate_Element kind=UNIVERSE)
	Builds a grid having the specified properties.
	Grid (const Congruence_System &cgs)
	Builds a grid, copying a system of congruences.
	Grid (Congruence_System &cgs, Recycle_Input dummy)
	Builds a grid, recycling a system of congruences.
	Grid (const Constraint_System &cs)
	Builds a grid, copying a system of constraints.
	Grid (Constraint_System &cs, Recycle_Input dummy)
	Builds a grid, recycling a system of constraints.
	Grid (const Grid_Generator_System &ggs)
	Builds a grid, copying a system of grid generators.
	Grid (Grid_Generator_System &ggs, Recycle_Input dummy)
	Builds a grid, recycling a system of grid generators.
template<typename Interval >
	Grid (const Box< Interval > &box, Complexity_Class complexity=ANY_COMPLEXITY)
	Builds a grid out of a box.
template<typename U >
	Grid (const BD_Shape< U > &bd, Complexity_Class complexity=ANY_COMPLEXITY)
	Builds a grid out of a bounded-difference shape.
template<typename U >
	Grid (const Octagonal_Shape< U > &os, Complexity_Class complexity=ANY_COMPLEXITY)
	Builds a grid out of an octagonal shape.
	Grid (const Polyhedron &ph, Complexity_Class complexity=ANY_COMPLEXITY)
	Builds a grid from a polyhedron using algorithms whose complexity does not exceed the one specified by `complexity`. If `complexity` is `ANY_COMPLEXITY`, then the grid built is the smallest one containing `ph`.
	Grid (const Grid &y, Complexity_Class complexity=ANY_COMPLEXITY)
	Ordinary copy constructor.
Grid &	operator= (const Grid &y)
	The assignment operator. (`*this` and `y` can be dimension-incompatible.)
Member Functions that Do Not Modify the Grid
dimension_type	space_dimension () const
	Returns the dimension of the vector space enclosing `*this`.
dimension_type	affine_dimension () const
	Returns , if `this` is empty; otherwise, returns the affine dimension of `this`.
Constraint_System	constraints () const
	Returns a system of equality constraints satisfied by `this` with the same affine dimension as `this`.
Constraint_System	minimized_constraints () const
	Returns a minimal system of equality constraints satisfied by `this` with the same affine dimension as `this`.
const Congruence_System &	congruences () const
	Returns the system of congruences.
const Congruence_System &	minimized_congruences () const
	Returns the system of congruences in minimal form.
const Grid_Generator_System &	grid_generators () const
	Returns the system of generators.
const Grid_Generator_System &	minimized_grid_generators () const
	Returns the minimized system of generators.
Poly_Con_Relation	relation_with (const Congruence &cg) const
	Returns the relations holding between `*this` and `cg`.
Poly_Gen_Relation	relation_with (const Grid_Generator &g) const
	Returns the relations holding between `*this` and `g`.
Poly_Gen_Relation	relation_with (const Generator &g) const
	Returns the relations holding between `*this` and `g`.
Poly_Con_Relation	relation_with (const Constraint &c) const
	Returns the relations holding between `*this` and `c`.
bool	is_empty () const
	Returns `true` if and only if `*this` is an empty grid.
bool	is_universe () const
	Returns `true` if and only if `*this` is a universe grid.
bool	is_topologically_closed () const
	Returns `true` if and only if `*this` is a topologically closed subset of the vector space.
bool	is_disjoint_from (const Grid &y) const
	Returns `true` if and only if `*this` and `y` are disjoint.
bool	is_discrete () const
	Returns `true` if and only if `*this` is discrete.
bool	is_bounded () const
	Returns `true` if and only if `*this` is bounded.
bool	contains_integer_point () const
	Returns `true` if and only if `*this` contains at least one integer point.
bool	constrains (Variable var) const
	Returns `true` if and only if `var` is constrained in `*this`.
bool	bounds_from_above (const Linear_Expression &expr) const
	Returns `true` if and only if `expr` is bounded in `*this`.
bool	bounds_from_below (const Linear_Expression &expr) const
	Returns `true` if and only if `expr` is bounded in `*this`.
bool	maximize (const Linear_Expression &expr, Coefficient &sup_n, Coefficient &sup_d, bool &maximum) const
	Returns `true` if and only if `this` is not empty and `expr` is bounded from above in `this`, in which case the supremum value is computed.
bool	maximize (const Linear_Expression &expr, Coefficient &sup_n, Coefficient &sup_d, bool &maximum, Generator &point) const
	Returns `true` if and only if `this` is not empty and `expr` is bounded from above in `this`, in which case the supremum value and a point where `expr` reaches it are computed.
bool	minimize (const Linear_Expression &expr, Coefficient &inf_n, Coefficient &inf_d, bool &minimum) const
	Returns `true` if and only if `this` is not empty and `expr` is bounded from below in `this`, in which case the infimum value is computed.
bool	minimize (const Linear_Expression &expr, Coefficient &inf_n, Coefficient &inf_d, bool &minimum, Generator &point) const
	Returns `true` if and only if `this` is not empty and `expr` is bounded from below in `this`, in which case the infimum value and a point where `expr` reaches it are computed.
bool	frequency (const Linear_Expression &expr, Coefficient &freq_n, Coefficient &freq_d, Coefficient &val_n, Coefficient &val_d) const
	Returns `true` if and only if `this` is not empty and frequency for `this` with respect to `expr` is defined, in which case the frequency and the value for `expr` that is closest to zero are computed.
bool	contains (const Grid &y) const
	Returns `true` if and only if `*this` contains `y`.
bool	strictly_contains (const Grid &y) const
	Returns `true` if and only if `*this` strictly contains `y`.
bool	OK (bool check_not_empty=false) const
	Checks if all the invariants are satisfied.
Space Dimension Preserving Member Functions that May Modify the Grid
void	add_congruence (const Congruence &cg)
	Adds a copy of congruence `cg` to `*this`.
void	add_grid_generator (const Grid_Generator &g)
	Adds a copy of grid generator `g` to the system of generators of `*this`.
void	add_congruences (const Congruence_System &cgs)
	Adds a copy of each congruence in `cgs` to `*this`.
void	add_recycled_congruences (Congruence_System &cgs)
	Adds the congruences in `cgs` to *this.
void	add_constraint (const Constraint &c)
	Adds to `*this` a congruence equivalent to constraint `c`.
void	add_constraints (const Constraint_System &cs)
	Adds to `*this` congruences equivalent to the constraints in `cs`.
void	add_recycled_constraints (Constraint_System &cs)
	Adds to `*this` congruences equivalent to the constraints in `cs`.
void	refine_with_congruence (const Congruence &cg)
	Uses a copy of the congruence `cg` to refine `*this`.
void	refine_with_congruences (const Congruence_System &cgs)
	Uses a copy of the congruences in `cgs` to refine `*this`.
void	refine_with_constraint (const Constraint &c)
	Uses a copy of the constraint `c` to refine `*this`.
void	refine_with_constraints (const Constraint_System &cs)
	Uses a copy of the constraints in `cs` to refine `*this`.
void	add_grid_generators (const Grid_Generator_System &gs)
	Adds a copy of the generators in `gs` to the system of generators of `*this`.
void	add_recycled_grid_generators (Grid_Generator_System &gs)
	Adds the generators in `gs` to the system of generators of `*this`.
void	unconstrain (Variable var)
	Computes the cylindrification of `this` with respect to space dimension `var`, assigning the result to `this`.
void	unconstrain (const Variables_Set &vars)
	Computes the cylindrification of `this` with respect to the set of space dimensions `vars`, assigning the result to `this`.
void	intersection_assign (const Grid &y)
	Assigns to `this` the intersection of `this` and `y`.
void	upper_bound_assign (const Grid &y)
	Assigns to `this` the least upper bound of `this` and `y`.
bool	upper_bound_assign_if_exact (const Grid &y)
	If the upper bound of `this` and `y` is exact it is assigned to `this` and `true` is returned, otherwise `false` is returned.
void	difference_assign (const Grid &y)
	Assigns to `this` the grid-difference of `this` and `y`.
bool	simplify_using_context_assign (const Grid &y)
	Assigns to `this` a meet-preserving simplification of `this` with respect to `y`. If `false` is returned, then the intersection is empty.
void	affine_image (Variable var, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one())
	Assigns to `this` the affine image of `this` under the function mapping variable `var` to the affine expression specified by `expr` and `denominator`.
void	affine_preimage (Variable var, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one())
	Assigns to `this` the affine preimage of `this` under the function mapping variable `var` to the affine expression specified by `expr` and `denominator`.
void	generalized_affine_image (Variable var, Relation_Symbol relsym, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one(), Coefficient_traits::const_reference modulus=Coefficient_zero())
	Assigns to `this` the image of `this` with respect to the generalized affine relation $\mathrm{var}' = \frac{\mathrm{expr}}{\mathrm{denominator}} \pmod{\mathrm{modulus}}$ .
void	generalized_affine_preimage (Variable var, Relation_Symbol relsym, const Linear_Expression &expr, Coefficient_traits::const_reference denominator=Coefficient_one(), Coefficient_traits::const_reference modulus=Coefficient_zero())
	Assigns to `this` the preimage of `this` with respect to the generalized affine relation $\mathrm{var}' = \frac{\mathrm{expr}}{\mathrm{denominator}} \pmod{\mathrm{modulus}}$ .
void	generalized_affine_image (const Linear_Expression &lhs, Relation_Symbol relsym, const Linear_Expression &rhs, Coefficient_traits::const_reference modulus=Coefficient_zero())
	Assigns to `this` the image of `this` with respect to the generalized affine relation $\mathrm{lhs}' = \mathrm{rhs} \pmod{\mathrm{modulus}}$ .
void	generalized_affine_preimage (const Linear_Expression &lhs, Relation_Symbol relsym, const Linear_Expression &rhs, Coefficient_traits::const_reference modulus=Coefficient_zero())
	Assigns to `this` the preimage of `this` with respect to the generalized affine relation $\mathrm{lhs}' = \mathrm{rhs} \pmod{\mathrm{modulus}}$ .
void	bounded_affine_image (Variable var, const Linear_Expression &lb_expr, const Linear_Expression &ub_expr, Coefficient_traits::const_reference denominator=Coefficient_one())
	Assigns to `this` the image of `this` with respect to the bounded affine relation $\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}$ .
void	bounded_affine_preimage (Variable var, const Linear_Expression &lb_expr, const Linear_Expression &ub_expr, Coefficient_traits::const_reference denominator=Coefficient_one())
	Assigns to `this` the preimage of `this` with respect to the bounded affine relation $\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}$ .
void	time_elapse_assign (const Grid &y)
	Assigns to `this` the result of computing the time-elapse between `this` and `y`.
void	wrap_assign (const Variables_Set &vars, Bounded_Integer_Type_Width w, Bounded_Integer_Type_Representation r, Bounded_Integer_Type_Overflow o, const Constraint_System *cs_p=0, unsigned complexity_threshold=16, bool wrap_individually=true)
	Wraps the specified dimensions of the vector space.
void	drop_some_non_integer_points (Complexity_Class complexity=ANY_COMPLEXITY)
	Possibly tightens `*this` by dropping all points with non-integer coordinates.
void	drop_some_non_integer_points (const Variables_Set &vars, Complexity_Class complexity=ANY_COMPLEXITY)
	Possibly tightens `*this` by dropping all points with non-integer coordinates for the space dimensions corresponding to `vars`.
void	topological_closure_assign ()
	Assigns to `*this` its topological closure.
void	congruence_widening_assign (const Grid &y, unsigned *tp=NULL)
	Assigns to `this` the result of computing the Grid widening between `this` and `y` using congruence systems.
void	generator_widening_assign (const Grid &y, unsigned *tp=NULL)
	Assigns to `this` the result of computing the Grid widening between `this` and `y` using generator systems.
void	widening_assign (const Grid &y, unsigned *tp=NULL)
	Assigns to `this` the result of computing the Grid widening between `this` and `y`.
void	limited_congruence_extrapolation_assign (const Grid &y, const Congruence_System &cgs, unsigned *tp=NULL)
	Improves the result of the congruence variant of Grid widening computation by also enforcing those congruences in `cgs` that are satisfied by all the points of `*this`.
void	limited_generator_extrapolation_assign (const Grid &y, const Congruence_System &cgs, unsigned *tp=NULL)
	Improves the result of the generator variant of the Grid widening computation by also enforcing those congruences in `cgs` that are satisfied by all the points of `*this`.
void	limited_extrapolation_assign (const Grid &y, const Congruence_System &cgs, unsigned *tp=NULL)
	Improves the result of the Grid widening computation by also enforcing those congruences in `cgs` that are satisfied by all the points of `*this`.
Member Functions that May Modify the Dimension of the Vector Space
void	add_space_dimensions_and_embed (dimension_type m)
	Adds `m` new space dimensions and embeds the old grid in the new vector space.
void	add_space_dimensions_and_project (dimension_type m)
	Adds `m` new space dimensions to the grid and does not embed it in the new vector space.
void	concatenate_assign (const Grid &y)
	Assigns to `this` the concatenation of `this` and `y`, taken in this order.
void	remove_space_dimensions (const Variables_Set &vars)
	Removes all the specified dimensions from the vector space.
void	remove_higher_space_dimensions (dimension_type new_dimension)
	Removes the higher dimensions of the vector space so that the resulting space will have dimension `new_dimension`..
template<typename Partial_Function >
void	map_space_dimensions (const Partial_Function &pfunc)
	Remaps the dimensions of the vector space according to a partial function.
void	expand_space_dimension (Variable var, dimension_type m)
	Creates `m` copies of the space dimension corresponding to `var`.
void	fold_space_dimensions (const Variables_Set &vars, Variable dest)
	Folds the space dimensions in `vars` into `dest`.
Miscellaneous Member Functions
	~Grid ()
	Destructor.
void	m_swap (Grid &y)
	Swaps `this` with grid `y`. (`this` and `y` can be dimension-incompatible.)
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 (as produced by ascii_dump(std::ostream&) const) and sets `*this` accordingly. Returns `true` if successful, `false` otherwise.
memory_size_type	total_memory_in_bytes () const
	Returns 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`.
int32_t	hash_code () const
	Returns a 32-bit hash code for `*this`.
Static Public Member Functions
static dimension_type	max_space_dimension ()
	Returns the maximum space dimension all kinds of Grid can handle.
static bool	can_recycle_congruence_systems ()
	Returns true indicating that this domain has methods that can recycle congruences.
static bool	can_recycle_constraint_systems ()
	Returns true indicating that this domain has methods that can recycle constraints.
Private Types
enum	Dimension_Kind { PARAMETER = 0, LINE = 1, GEN_VIRTUAL = 2, PROPER_CONGRUENCE = PARAMETER, CON_VIRTUAL = LINE, EQUALITY = GEN_VIRTUAL }
enum	Three_Valued_Boolean { TVB_TRUE, TVB_FALSE, TVB_DONT_KNOW }
typedef std::vector < Dimension_Kind >	Dimension_Kinds
Private Member Functions
void	construct (dimension_type num_dimensions, Degenerate_Element kind)
	Builds a grid universe or empty grid.
void	construct (Congruence_System &cgs)
	Builds a grid from a system of congruences.
void	construct (Grid_Generator_System &ggs)
	Builds a grid from a system of grid generators.
Three_Valued_Boolean	quick_equivalence_test (const Grid &y) const
	Polynomial but incomplete equivalence test between grids.
bool	is_included_in (const Grid &y) const
	Returns `true` if and only if `*this` is included in `y`.
bool	bounds (const Linear_Expression &expr, const char *method_call) const
	Checks if and how `expr` is bounded in `*this`.
bool	max_min (const Linear_Expression &expr, const char method_call, Coefficient &ext_n, Coefficient &ext_d, bool &included, Generator point=NULL) const
	Maximizes or minimizes `expr` subject to `*this`.
bool	frequency_no_check (const Linear_Expression &expr, Coefficient &freq_n, Coefficient &freq_d, Coefficient &val_n, Coefficient &val_d) const
	Returns `true` if and only if `this` is not empty and frequency for `this` with respect to `expr` is defined, in which case the frequency and the value for `expr` that is closest to zero are computed.
bool	bounds_no_check (const Linear_Expression &expr) const
	Checks if and how `expr` is bounded in `*this`.
void	add_congruence_no_check (const Congruence &cg)
	Adds the congruence `cg` to `*this`.
void	add_constraint_no_check (const Constraint &c)
	Uses the constraint `c` to refine `*this`.
void	refine_no_check (const Constraint &c)
	Uses the constraint `c` to refine `*this`.
void	add_space_dimensions (Congruence_System &cgs, Grid_Generator_System &gs, dimension_type dims)
	Adds new space dimensions to the given systems.
void	add_space_dimensions (Grid_Generator_System &gs, Congruence_System &cgs, dimension_type dims)
	Adds new space dimensions to the given systems.
Private Verifiers: Verify if Individual Flags are Set
bool	marked_empty () const
	Returns `true` if the grid is known to be empty.
bool	congruences_are_up_to_date () const
	Returns `true` if the system of congruences is up-to-date.
bool	generators_are_up_to_date () const
	Returns `true` if the system of generators is up-to-date.
bool	congruences_are_minimized () const
	Returns `true` if the system of congruences is minimized.
bool	generators_are_minimized () const
	Returns `true` if the system of generators is minimized.
State Flag Setters: Set Only the Specified Flags
void	set_zero_dim_univ ()
	Sets `status` to express that the grid is the universe 0-dimension vector space, clearing all corresponding matrices.
void	set_empty ()
	Sets `status` to express that the grid is empty, clearing all corresponding matrices.
void	set_congruences_up_to_date ()
	Sets `status` to express that congruences are up-to-date.
void	set_generators_up_to_date ()
	Sets `status` to express that generators are up-to-date.
void	set_congruences_minimized ()
	Sets `status` to express that congruences are minimized.
void	set_generators_minimized ()
	Sets `status` to express that generators are minimized.
State Flag Cleaners: Clear Only the Specified Flag
void	clear_empty ()
	Clears the `status` flag indicating that the grid is empty.
void	clear_congruences_up_to_date ()
	Sets `status` to express that congruences are out of date.
void	clear_generators_up_to_date ()
	Sets `status` to express that generators are out of date.
void	clear_congruences_minimized ()
	Sets `status` to express that congruences are no longer minimized.
void	clear_generators_minimized ()
	Sets `status` to express that generators are no longer minimized.
Updating Matrices
void	update_congruences () const
	Updates and minimizes the congruences from the generators.
bool	update_generators () const
	Updates and minimizes the generators from the congruences.
Minimization of Descriptions
bool	minimize () const
	Minimizes both the congruences and the generators.
Widening- and Extrapolation-Related Functions
void	select_wider_congruences (const Grid &y, Congruence_System &selected_cgs) const
	Copies a widened selection of congruences from `y` to `selected_cgs`.
void	select_wider_generators (const Grid &y, Grid_Generator_System &widened_ggs) const
	Copies widened generators from `y` to `widened_ggs`.
Static Private Member Functions
Minimization-related Static Member Functions
static void	normalize_divisors (Grid_Generator_System &sys, Coefficient &divisor, const Grid_Generator *first_point=NULL)
	Normalizes the divisors in `sys`.
static void	normalize_divisors (Grid_Generator_System &sys)
	Normalizes the divisors in `sys`.
static void	normalize_divisors (Grid_Generator_System &sys, Grid_Generator_System &gen_sys)
	Normalize all the divisors in `sys` and `gen_sys`.
static void	conversion (Congruence_System &source, Grid_Generator_System &dest, Dimension_Kinds &dim_kinds)
	Converts generator system `dest` to be equivalent to congruence system `source`.
static void	conversion (Grid_Generator_System &source, Congruence_System &dest, Dimension_Kinds &dim_kinds)
	Converts congruence system `dest` to be equivalent to generator system `source`.
static bool	simplify (Congruence_System &cgs, Dimension_Kinds &dim_kinds)
	Converts `cgs` to upper triangular (i.e. minimized) form.
static void	simplify (Grid_Generator_System &ggs, Dimension_Kinds &dim_kinds)
	Converts `gs` to lower triangular (i.e. minimized) form.
static void	reduce_line_with_line (Grid_Generator &row, Grid_Generator &pivot, dimension_type column)
	Reduces the line `row` using the line `pivot`.
static void	reduce_equality_with_equality (Congruence &row, const Congruence &pivot, dimension_type column)
	Reduces the equality `row` using the equality `pivot`.
template<typename R >
static void	reduce_pc_with_pc (R &row, R &pivot, dimension_type column, dimension_type start, dimension_type end)
	Reduces `row` using `pivot`.
static void	reduce_parameter_with_line (Grid_Generator &row, const Grid_Generator &pivot, dimension_type column, Grid_Generator_System &sys)
	Reduce `row` using `pivot`.
static void	reduce_congruence_with_equality (Congruence &row, const Congruence &pivot, dimension_type column, Congruence_System &sys)
	Reduce `row` using `pivot`.
template<typename M , typename R >
static void	reduce_reduced (M &sys, dimension_type dim, dimension_type pivot_index, dimension_type start, dimension_type end, const Dimension_Kinds &sys_dim_kinds, bool generators=true)
	Reduce column `dim` in rows preceding `pivot_index` in `sys`.
static void	multiply_grid (const Coefficient &multiplier, Congruence &cg, Congruence_System &dest, dimension_type num_rows, dimension_type num_dims)
	Multiply the elements of `dest` by `multiplier`.
static void	multiply_grid (const Coefficient &multiplier, Grid_Generator &gen, Grid_Generator_System &dest, dimension_type num_rows, dimension_type num_dims)
	Multiply the elements of `dest` by `multiplier`.
static bool	lower_triangular (const Congruence_System &sys, const Dimension_Kinds &dim_kinds)
	If `sys` is lower triangular return `true`, else return `false`.
static bool	upper_triangular (const Grid_Generator_System &sys, const Dimension_Kinds &dim_kinds)
	If `sys` is upper triangular return `true`, else return `false`.
template<typename M , typename R >
static bool	rows_are_zero (M &system, dimension_type first, dimension_type last, dimension_type row_size)
	Checks that trailing rows contain only zero terms.
Private Attributes
Congruence_System	con_sys
	The system of congruences.
Grid_Generator_System	gen_sys
	The system of generators.
Status	status
	The status flags to keep track of the grid's internal state.
dimension_type	space_dim
	The number of dimensions of the enclosing vector space.
Dimension_Kinds	dim_kinds
Friends
class	Parma_Polyhedra_Library::Grid_Certificate
class	Parma_Polyhedra_Library::Box
bool	operator== (const Grid &x, const Grid &y)
Related Functions
(Note that these are not member functions.)
std::ostream &	operator<< (std::ostream &s, const Grid &gr)
	Output operator.
void	swap (Grid &x, Grid &y)
	Swaps `x` with `y`.
bool	operator== (const Grid &x, const Grid &y)
	Returns `true` if and only if `x` and `y` are the same grid.
bool	operator!= (const Grid &x, const Grid &y)
	Returns `true` if and only if `x` and `y` are different grids.
bool	operator!= (const Grid &x, const Grid &y)
void	swap (Grid &x, Grid &y)
bool	operator== (const Grid &x, const Grid &y)
std::ostream &	operator<< (std::ostream &s, const Grid &gr)
Exception Throwers
void	throw_dimension_incompatible (const char method, const char other_name, dimension_type other_dim) const
void	throw_dimension_incompatible (const char method, const char gr_name, const Grid &gr) const
void	throw_dimension_incompatible (const char method, const char le_name, const Linear_Expression &le) const
void	throw_dimension_incompatible (const char method, const char cg_name, const Congruence &cg) const
void	throw_dimension_incompatible (const char method, const char c_name, const Constraint &c) const
void	throw_dimension_incompatible (const char method, const char g_name, const Grid_Generator &g) const
void	throw_dimension_incompatible (const char method, const char g_name, const Generator &g) const
void	throw_dimension_incompatible (const char method, const char cgs_name, const Congruence_System &cgs) const
void	throw_dimension_incompatible (const char method, const char cs_name, const Constraint_System &cs) const
void	throw_dimension_incompatible (const char method, const char gs_name, const Grid_Generator_System &gs) const
void	throw_dimension_incompatible (const char method, const char var_name, Variable var) const
void	throw_dimension_incompatible (const char *method, dimension_type required_space_dim) const
static void	throw_invalid_argument (const char method, const char reason)
static void	throw_invalid_constraint (const char method, const char c_name)
static void	throw_invalid_constraints (const char method, const char cs_name)
static void	throw_invalid_generator (const char method, const char g_name)
static void	throw_invalid_generators (const char method, const char gs_name)

Detailed Description

A grid.

An object of the class Grid represents a rational grid.

The domain of grids optimally supports:

all (proper and non-proper) congruences;
tautological and inconsistent constraints;
linear equality constraints (i.e., non-proper congruences).

Depending on the method, using a constraint that is not optimally supported by the domain will either raise an exception or result in a (possibly non-optimal) upward approximation.

The domain of grids support a concept of double description similar to the one developed for polyhedra: hence, a grid can be specified as either a finite system of congruences or a finite system of generators (see Section Rational Grids) and it is always possible to obtain either representation. That is, if we know the system of congruences, we can obtain from this a system of generators that define the same grid and vice versa. These systems can contain redundant members, or they can be in the minimal form.

A key attribute of any grid is its space dimension (the dimension $n \in \Nset$ of the enclosing vector space):

all grids, the empty ones included, are endowed with a space dimension;
most operations working on a grid and another object (another grid, a congruence, a generator, a set of variables, etc.) will throw an exception if the grid and the object are not dimension-compatible (see Section Space Dimensions and Dimension-compatibility for Grids);
the only ways in which the space dimension of a grid can be changed are with explicit calls to operators provided for that purpose, and with standard copy, assignment and swap operators.

Note that two different grids can be defined on the zero-dimension space: the empty grid and the universe grid $R^0$ .

In all the examples it is assumed that variables x and y are defined (where they are used) as follows:

  Variable x(0);
  Variable y(1);

Example 1

The following code builds a grid corresponding to the even integer pairs in $\Rset^2$ , given as a system of congruences:

  Congruence_System cgs;
  cgs.insert((x %= 0) / 2);
  cgs.insert((y %= 0) / 2);
  Grid gr(cgs);

The following code builds the same grid as above, but starting from a system of generators specifying three of the points:

  Grid_Generator_System gs;
  gs.insert(grid_point(0*x + 0*y));
  gs.insert(grid_point(0*x + 2*y));
  gs.insert(grid_point(2*x + 0*y));
  Grid gr(gs);

Example 2

The following code builds a grid corresponding to a line in $\Rset^2$ by adding a single congruence to the universe grid:

  Congruence_System cgs;
  cgs.insert(x - y == 0);
  Grid gr(cgs);

The following code builds the same grid as above, but starting from a system of generators specifying a point and a line:

  Grid_Generator_System gs;
  gs.insert(grid_point(0*x + 0*y));
  gs.insert(grid_line(x + y));
  Grid gr(gs);

Example 3

The following code builds a grid corresponding to the integral points on the line $x = y$

in $\Rset^2$ constructed by adding an equality and congruence to the universe grid:

  Congruence_System cgs;
  cgs.insert(x - y == 0);
  cgs.insert(x %= 0);
  Grid gr(cgs);

The following code builds the same grid as above, but starting from a system of generators specifying a point and a parameter:

  Grid_Generator_System gs;
  gs.insert(grid_point(0*x + 0*y));
  gs.insert(parameter(x + y));
  Grid gr(gs);

Example 4

The following code builds the grid corresponding to a plane by creating the universe grid in $\Rset^2$ :

  Grid gr(2);

The following code builds the same grid as above, but starting from the empty grid in $\Rset^2$ and inserting the appropriate generators (a point, and two lines).

  Grid gr(2, EMPTY);
  gr.add_grid_generator(grid_point(0*x + 0*y));
  gr.add_grid_generator(grid_line(x));
  gr.add_grid_generator(grid_line(y));

Note that a generator system must contain a point when describing a grid. To ensure that this is always the case it is required that the first generator inserted in an empty grid is a point (otherwise, an exception is thrown).

Example 5

The following code shows the use of the function add_space_dimensions_and_embed:

  Grid gr(1);
  gr.add_congruence(x == 2);
  gr.add_space_dimensions_and_embed(1);

We build the universe grid in the 1-dimension space $\Rset$ . Then we add a single equality congruence, thus obtaining the grid corresponding to the singleton set $\{ 2 \} \sseq \Rset$ . After the last line of code, the resulting grid is

$\bigl\{\, (2, y)^\transpose \in \Rset^2 \bigm| y \in \Rset \,\bigr\}.$

Example 6

The following code shows the use of the function add_space_dimensions_and_project:

  Grid gr(1);
  gr.add_congruence(x == 2);
  gr.add_space_dimensions_and_project(1);

The first two lines of code are the same as in Example 4 for add_space_dimensions_and_embed. After the last line of code, the resulting grid is the singleton set $\bigl\{ (2, 0)^\transpose \bigr\} \sseq \Rset^2$ .

Example 7

The following code shows the use of the function affine_image:

  Grid gr(2, EMPTY);
  gr.add_grid_generator(grid_point(0*x + 0*y));
  gr.add_grid_generator(grid_point(4*x + 0*y));
  gr.add_grid_generator(grid_point(0*x + 2*y));
  Linear_Expression expr = x + 3;
  gr.affine_image(x, expr);

In this example the starting grid is all the pairs of $x$

and

in $\Rset^2$ where $x$

is an integer multiple of 4 and $y$

is an integer multiple of 2. The considered variable is $x$

and the affine expression is $x+3$

. The resulting grid is the given grid translated 3 integers to the right (all the pairs $(x, y)$

where

is -1 plus an integer multiple of 4 and $y$

is an integer multiple of 2). Moreover, if the affine transformation for the same variable x is instead $x+y$

:

  Linear_Expression expr = x + y;

the resulting grid is every second integral point along the $x=y$

line, with this line of points repeated at every fourth integral value along the $x$

axis. Instead, if we do not use an invertible transformation for the same variable; for example, the affine expression $y$

:

  Linear_Expression expr = y;

the resulting grid is every second point along the $x=y$

line.

Example 8

The following code shows the use of the function affine_preimage:

  Grid gr(2, EMPTY);
  gr.add_grid_generator(grid_point(0*x + 0*y));
  gr.add_grid_generator(grid_point(4*x + 0*y));
  gr.add_grid_generator(grid_point(0*x + 2*y));
  Linear_Expression expr = x + 3;
  gr.affine_preimage(x, expr);

In this example the starting grid, var and the affine expression and the denominator are the same as in Example 6, while the resulting grid is similar but translated 3 integers to the left (all the pairs $(x, y)$

where

is -3 plus an integer multiple of 4 and $y$

is an integer multiple of 2).. Moreover, if the affine transformation for x is $x+y$

  Linear_Expression expr = x + y;

the resulting grid is a similar grid to the result in Example 6, only the grid is slanted along $x=-y$

. Instead, if we do not use an invertible transformation for the same variable x, for example, the affine expression $y$

:

  Linear_Expression expr = y;

the resulting grid is every fourth line parallel to the $x$

axis.

Example 9

For this example we also use the variables:

  Variable z(2);
  Variable w(3);

The following code shows the use of the function remove_space_dimensions:

  Grid_Generator_System gs;
  gs.insert(grid_point(3*x + y +0*z + 2*w));
  Grid gr(gs);
  Variables_Set vars;
  vars.insert(y);
  vars.insert(z);
  gr.remove_space_dimensions(vars);

The starting grid is the singleton set $\bigl\{ (3, 1, 0, 2)^\transpose \bigr\} \sseq \Rset^4$ , while the resulting grid is $\bigl\{ (3, 2)^\transpose \bigr\} \sseq \Rset^2$ . Be careful when removing space dimensions incrementally: since dimensions are automatically renamed after each application of the remove_space_dimensions operator, unexpected results can be obtained. For instance, by using the following code we would obtain a different result:

  set<Variable> vars1;
  vars1.insert(y);
  gr.remove_space_dimensions(vars1);
  set<Variable> vars2;
  vars2.insert(z);
  gr.remove_space_dimensions(vars2);

In this case, the result is the grid $\bigl\{(3, 0)^\transpose \bigr\} \sseq \Rset^2$ : when removing the set of dimensions vars2 we are actually removing variable $w$

of the original grid. For the same reason, the operator remove_space_dimensions is not idempotent: removing twice the same non-empty set of dimensions is never the same as removing them just once.

Definition at line 363 of file Grid.defs.hh.

Member Typedef Documentation

typedef Coefficient Parma_Polyhedra_Library::Grid::coefficient_type

The numeric type of coefficients.

Definition at line 366 of file Grid.defs.hh.

typedef std::vector<Dimension_Kind> Parma_Polyhedra_Library::Grid::Dimension_Kinds

private

Definition at line 1994 of file Grid.defs.hh.

Member Enumeration Documentation

enum Parma_Polyhedra_Library::Grid::Dimension_Kind

private

Enumerator:

PARAMETER
LINE
GEN_VIRTUAL
PROPER_CONGRUENCE
CON_VIRTUAL
EQUALITY

Definition at line 1985 of file Grid.defs.hh.

                      {
    PARAMETER = 0,
    LINE = 1,
    GEN_VIRTUAL = 2,
    PROPER_CONGRUENCE = PARAMETER,
    CON_VIRTUAL = LINE,
    EQUALITY = GEN_VIRTUAL
  };

enum Parma_Polyhedra_Library::Grid::Three_Valued_Boolean

private

Enumerator:

TVB_TRUE
TVB_FALSE
TVB_DONT_KNOW

Definition at line 2142 of file Grid.defs.hh.

                            {
    TVB_TRUE,
    TVB_FALSE,
    TVB_DONT_KNOW
  };

Constructor & Destructor Documentation

Parma_Polyhedra_Library::Grid::Grid	(	dimension_type	num_dimensions = `0`,
		Degenerate_Element	kind = `UNIVERSE`
	)

inlineexplicit

Builds a grid having the specified properties.

Parameters:

num_dimensions	The number of dimensions of the vector space enclosing the grid;
kind	Specifies whether the universe or the empty grid has to be built.

Exceptions:

std::length_error Thrown if num_dimensions exceeds the maximum allowed space dimension.

Definition at line 122 of file Grid.inlines.hh.

References construct(), OK(), and PPL_ASSERT.

  : con_sys(),
    gen_sys(check_space_dimension_overflow(num_dimensions,
                                           max_space_dimension(),
                                           "PPL::Grid::",
                                           "Grid(n, k)",
                                           "n exceeds the maximum "
                                           "allowed space dimension")) {
  construct(num_dimensions, kind);
  PPL_ASSERT(OK());
}

Parma_Polyhedra_Library::Grid::Grid ( const Congruence_System & cgs )

inlineexplicit

Builds a grid, copying a system of congruences.

The grid inherits the space dimension of the congruence system.

Parameters:

cgs	The system of congruences defining the grid.

Exceptions:

std::length_error Thrown if num_dimensions exceeds the maximum allowed space dimension.

Definition at line 136 of file Grid.inlines.hh.

References construct().

  : con_sys(check_space_dimension_overflow(cgs.space_dimension(),
                                           max_space_dimension(),
                                           "PPL::Grid::",
                                           "Grid(cgs)",
                                           "the space dimension of cgs "
                                           "exceeds the maximum allowed "
                                           "space dimension")),
    gen_sys(cgs.space_dimension()) {
  Congruence_System cgs_copy(cgs);
  construct(cgs_copy);
}

Parma_Polyhedra_Library::Grid::Grid	(	Congruence_System &	cgs,
		Recycle_Input	dummy
	)

inline

Builds a grid, recycling a system of congruences.

The grid inherits the space dimension of the congruence system.

Parameters:

cgs	The system of congruences defining the grid. Its data-structures may be recycled to build the grid.
dummy	A dummy tag to syntactically differentiate this one from the other constructors.

Exceptions:

std::length_error Thrown if num_dimensions exceeds the maximum allowed space dimension.

Definition at line 150 of file Grid.inlines.hh.

References construct().

  : con_sys(check_space_dimension_overflow(cgs.space_dimension(),
                                           max_space_dimension(),
                                           "PPL::Grid::",
                                           "Grid(cgs, recycle)",
                                           "the space dimension of cgs "
                                           "exceeds the maximum allowed "
                                           "space dimension")),
    gen_sys(cgs.space_dimension()) {
  construct(cgs);
}

Parma_Polyhedra_Library::Grid::Grid ( const Constraint_System & cs )

explicit

Builds a grid, copying a system of constraints.

The grid inherits the space dimension of the constraint system.

Parameters:

cs	The system of constraints defining the grid.

Exceptions:

std::invalid_argument	Thrown if the constraint system `cs` contains inequality constraints.
std::length_error	Thrown if `num_dimensions` exceeds the maximum allowed space dimension.

Definition at line 59 of file Grid_public.cc.

References Parma_Polyhedra_Library::Constraint_System::begin(), con_sys, construct(), Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Congruence_System::insert(), OK(), PPL_ASSERT, Parma_Polyhedra_Library::Grid::Status::set_empty(), set_zero_dim_univ(), space_dim, Parma_Polyhedra_Library::Constraint_System::space_dimension(), status, throw_invalid_constraints(), and Parma_Polyhedra_Library::Congruence::zero_dim_false().

  : con_sys(check_space_dimension_overflow(cs.space_dimension(),
                                           max_space_dimension(),
                                           "PPL::Grid::",
                                           "Grid(cs)",
                                           "the space dimension of cs "
                                           "exceeds the maximum allowed "
                                           "space dimension")),
    gen_sys(cs.space_dimension()) {
  space_dim = cs.space_dimension();

  if (space_dim == 0) {
    // See if an inconsistent constraint has been passed.
    for (Constraint_System::const_iterator i = cs.begin(),
         cs_end = cs.end(); i != cs_end; ++i)
      if (i->is_inconsistent()) {
        // Inconsistent constraint found: the grid is empty.
        status.set_empty();
        // Insert the zero dim false congruence system into `con_sys'.
        // `gen_sys' is already in empty form.
        con_sys.insert(Congruence::zero_dim_false());
        PPL_ASSERT(OK());
        return;
      }
    set_zero_dim_univ();
    PPL_ASSERT(OK());
    return;
  }

  Congruence_System cgs;
  cgs.insert(0*Variable(space_dim - 1) %= 1);
  for (Constraint_System::const_iterator i = cs.begin(),
         cs_end = cs.end(); i != cs_end; ++i)
    if (i->is_equality())
      cgs.insert(*i);
    else
      throw_invalid_constraints("Grid(cs)", "cs");
  construct(cgs);
}

Parma_Polyhedra_Library::Grid::Grid	(	Constraint_System &	cs,
		Recycle_Input	dummy
	)

Builds a grid, recycling a system of constraints.

The grid inherits the space dimension of the constraint system.

Parameters:

cs	The system of constraints defining the grid. Its data-structures may be recycled to build the grid.
dummy	A dummy tag to syntactically differentiate this one from the other constructors.

Exceptions:

std::invalid_argument	Thrown if the constraint system `cs` contains inequality constraints.
std::length_error	Thrown if `num_dimensions` exceeds the maximum allowed space dimension.

Definition at line 99 of file Grid_public.cc.

References Parma_Polyhedra_Library::Constraint_System::begin(), con_sys, construct(), Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Congruence_System::insert(), OK(), PPL_ASSERT, Parma_Polyhedra_Library::Grid::Status::set_empty(), set_zero_dim_univ(), space_dim, Parma_Polyhedra_Library::Constraint_System::space_dimension(), status, throw_invalid_constraint(), and Parma_Polyhedra_Library::Congruence::zero_dim_false().

  : con_sys(check_space_dimension_overflow(cs.space_dimension(),
                                           max_space_dimension(),
                                           "PPL::Grid::",
                                           "Grid(cs, recycle)",
                                           "the space dimension of cs "
                                           "exceeds the maximum allowed "
                                           "space dimension")),
    gen_sys(cs.space_dimension()) {
  space_dim = cs.space_dimension();

  if (space_dim == 0) {
    // See if an inconsistent constraint has been passed.
    for (Constraint_System::const_iterator i = cs.begin(),
         cs_end = cs.end(); i != cs_end; ++i)
      if (i->is_inconsistent()) {
        // Inconsistent constraint found: the grid is empty.
        status.set_empty();
        // Insert the zero dim false congruence system into `con_sys'.
        // `gen_sys' is already in empty form.
        con_sys.insert(Congruence::zero_dim_false());
        PPL_ASSERT(OK());
        return;
      }
    set_zero_dim_univ();
    PPL_ASSERT(OK());
    return;
  }

  Congruence_System cgs;
  cgs.insert(0*Variable(space_dim - 1) %= 1);
  for (Constraint_System::const_iterator i = cs.begin(),
         cs_end = cs.end(); i != cs_end; ++i)
    if (i->is_equality())
      cgs.insert(*i);
    else
      throw_invalid_constraint("Grid(cs)", "cs");
  construct(cgs);
}

Parma_Polyhedra_Library::Grid::Grid ( const Grid_Generator_System & ggs )

inlineexplicit

Builds a grid, copying a system of grid generators.

The grid inherits the space dimension of the generator system.

Parameters:

ggs	The system of generators defining the grid.

Exceptions:

std::invalid_argument	Thrown if the system of generators is not empty but has no points.
std::length_error	Thrown if `num_dimensions` exceeds the maximum allowed space dimension.

Definition at line 163 of file Grid.inlines.hh.

References construct().

  : con_sys(check_space_dimension_overflow(ggs.space_dimension(),
                                           max_space_dimension(),
                                           "PPL::Grid::",
                                           "Grid(ggs)",
                                           "the space dimension of ggs "
                                           "exceeds the maximum allowed "
                                           "space dimension")),
    gen_sys(ggs.space_dimension()) {
  Grid_Generator_System ggs_copy(ggs);
  construct(ggs_copy);
}

Parma_Polyhedra_Library::Grid::Grid	(	Grid_Generator_System &	ggs,
		Recycle_Input	dummy
	)

inline

Builds a grid, recycling a system of grid generators.

The grid inherits the space dimension of the generator system.

Parameters:

ggs	The system of generators defining the grid. Its data-structures may be recycled to build the grid.
dummy	A dummy tag to syntactically differentiate this one from the other constructors.

Exceptions:

std::invalid_argument	Thrown if the system of generators is not empty but has no points.
std::length_error	Thrown if `num_dimensions` exceeds the maximum allowed space dimension.

Definition at line 177 of file Grid.inlines.hh.

References construct().

  : con_sys(check_space_dimension_overflow(ggs.space_dimension(),
                                           max_space_dimension(),
                                           "PPL::Grid::",
                                           "Grid(ggs, recycle)",
                                           "the space dimension of ggs "
                                           "exceeds the maximum allowed "
                                           "space dimension")),
    gen_sys(ggs.space_dimension()) {
  construct(ggs);
}

template<typename Interval >

Parma_Polyhedra_Library::Grid::Grid	(	const Box< Interval > &	box,
		Complexity_Class	complexity = `ANY_COMPLEXITY`
	)

explicit

Builds a grid out of a box.

The grid inherits the space dimension of the box. The built grid is the most precise grid that includes the box.

Parameters:

box	The box representing the grid to be built.
complexity	This argument is ignored as the algorithm used has polynomial complexity.

Exceptions:

std::length_error Thrown if the space dimension of box exceeds the maximum allowed space dimension.

Definition at line 36 of file Grid.templates.hh.

  : con_sys(),
    gen_sys() {
  space_dim = check_space_dimension_overflow(box.space_dimension(),
                                             max_space_dimension(),
                                             "PPL::Grid::",
                                             "Grid(box, from_bounding_box)",
                                             "the space dimension of box "
                                             "exceeds the maximum allowed "
                                             "space dimension");

  if (box.is_empty()) {
    // Empty grid.
    set_empty();
    PPL_ASSERT(OK());
    return;
  }

  if (space_dim == 0)
    set_zero_dim_univ();
  else {
    // Initialize the space dimension as indicated by the box.
    con_sys.increase_space_dimension(space_dim);
    // Add congruences and generators according to `box'.
    PPL_DIRTY_TEMP_COEFFICIENT(l_n);
    PPL_DIRTY_TEMP_COEFFICIENT(l_d);
    PPL_DIRTY_TEMP_COEFFICIENT(u_n);
    PPL_DIRTY_TEMP_COEFFICIENT(u_d);
    gen_sys.insert(grid_point(0*Variable(space_dim-1)));
    for (dimension_type k = space_dim; k-- > 0; ) {
      const Variable v_k = Variable(k);
      // This is declared here because it may be invalidated by the call to
      // gen_sys.insert() at the end of the loop.
      bool closed = false;
      // TODO: Consider producing the system(s) in minimized form.
      if (box.has_lower_bound(v_k, l_n, l_d, closed)) {
        if (box.has_upper_bound(v_k, u_n, u_d, closed))
          if (l_n * u_d == u_n * l_d) {
            Grid_Generator& point = gen_sys[0];
            // A point interval sets dimension k of every point to a
            // single value.
            con_sys.insert(l_d * v_k == l_n);

            // Scale the point to use as divisor the lcm of the
            // divisors of the existing point and the lower bound.
            const Coefficient& point_divisor = point.divisor();
            gcd_assign(u_n, l_d, point_divisor);
            // `u_n' now holds the gcd.
            exact_div_assign(u_n, point_divisor, u_n);
            if (l_d < 0)
              neg_assign(u_n);
            // l_d * u_n == abs(l_d * (point_divisor / gcd(l_d, point_divisor)))
            point.scale_to_divisor(l_d * u_n);
            // Set dimension k of the point to the lower bound.
            if (l_d < 0)
              neg_assign(u_n);
            // point[k + 1] = l_n * point_divisor / gcd(l_d, point_divisor)
            point[k + 1] = l_n * u_n;

            continue;
          }
      }
      // A universe interval allows any value in dimension k.
      gen_sys.insert(grid_line(v_k));
    }
    set_congruences_up_to_date();
    set_generators_up_to_date();
    gen_sys.unset_pending_rows();
    gen_sys.set_sorted(false);
  }

  PPL_ASSERT(OK());
}

template<typename U >

Parma_Polyhedra_Library::Grid::Grid	(	const BD_Shape< U > &	bd,
		Complexity_Class	complexity = `ANY_COMPLEXITY`
	)

inlineexplicit

Builds a grid out of a bounded-difference shape.

The grid inherits the space dimension of the BDS. The built grid is the most precise grid that includes the BDS.

Parameters:

bd	The BDS representing the grid to be built.
complexity	This argument is ignored as the algorithm used has polynomial complexity.

Exceptions:

std::length_error Thrown if the space dimension of bd exceeds the maximum allowed space dimension.

Definition at line 191 of file Grid.inlines.hh.

References Parma_Polyhedra_Library::BD_Shape< T >::congruences(), and construct().

  : con_sys(check_space_dimension_overflow(bd.space_dimension(),
                                           max_space_dimension(),
                                           "PPL::Grid::",
                                           "Grid(bd)",
                                           "the space dimension of bd "
                                           "exceeds the maximum allowed "
                                           "space dimension")),
    gen_sys(bd.space_dimension()) {
  Congruence_System cgs = bd.congruences();
  construct(cgs);
}

template<typename U >

Parma_Polyhedra_Library::Grid::Grid	(	const Octagonal_Shape< U > &	os,
		Complexity_Class	complexity = `ANY_COMPLEXITY`
	)

inlineexplicit

Builds a grid out of an octagonal shape.

The grid inherits the space dimension of the octagonal shape. The built grid is the most precise grid that includes the octagonal shape.

Parameters:

os	The octagonal shape representing the grid to be built.
complexity	This argument is ignored as the algorithm used has polynomial complexity.

Exceptions:

std::length_error Thrown if the space dimension of os exceeds the maximum allowed space dimension.

Definition at line 206 of file Grid.inlines.hh.

References Parma_Polyhedra_Library::Octagonal_Shape< T >::congruences(), and construct().

  : con_sys(check_space_dimension_overflow(os.space_dimension(),
                                           max_space_dimension(),
                                           "PPL::Grid::",
                                           "Grid(os)",
                                           "the space dimension of os "
                                           "exceeds the maximum allowed "
                                           "space dimension")),
    gen_sys(os.space_dimension()) {
  Congruence_System cgs = os.congruences();
  construct(cgs);
}

Parma_Polyhedra_Library::Grid::Grid	(	const Polyhedron &	ph,
		Complexity_Class	complexity = `ANY_COMPLEXITY`
	)

explicit

Builds a grid from a polyhedron using algorithms whose complexity does not exceed the one specified by complexity. If complexity is ANY_COMPLEXITY, then the grid built is the smallest one containing ph.

The grid inherits the space dimension of polyhedron.

Parameters:

ph	The polyhedron.
complexity	The complexity class.

Exceptions:

std::length_error Thrown if num_dimensions exceeds the maximum allowed space dimension.

Definition at line 139 of file Grid_public.cc.

  : con_sys(check_space_dimension_overflow(ph.space_dimension(),
                                           max_space_dimension(),
                                           "PPL::Grid::",
                                           "Grid(ph)",
                                           "the space dimension of ph "
                                           "exceeds the maximum allowed "
                                           "space dimension")),
    gen_sys(ph.space_dimension()) {
  space_dim = ph.space_dimension();

  // A zero-dim polyhedron causes no complexity problems.
  if (space_dim == 0) {
    if (ph.is_empty())
      set_empty();
    else
      set_zero_dim_univ();
    return;
  }

  // A polyhedron known to be empty causes no complexity problems.
  if (ph.marked_empty()) {
    set_empty();
    return;
  }

  bool use_constraints = ph.constraints_are_minimized()
    || !ph.generators_are_up_to_date();

  // Minimize the constraint description if it is needed and
  // the complexity allows it.
  if (use_constraints && complexity == ANY_COMPLEXITY)
    if (!ph.minimize()) {
      set_empty();
      return;
    }

  if (use_constraints) {
    // Only the equality constraints need be used.
    PPL_ASSERT(ph.constraints_are_up_to_date());
    const Constraint_System& cs = ph.constraints();
    Congruence_System cgs;
    cgs.insert(0*Variable(space_dim - 1) %= 1);
    for (Constraint_System::const_iterator i = cs.begin(),
           cs_end = cs.end(); i != cs_end; ++i)
      if (i->is_equality())
        cgs.insert(*i);
    construct(cgs);
  }
  else {
    // First find a point or closure point and convert it to a
    // grid point and add to the (initially empty) set of grid generators.
    PPL_ASSERT(ph.generators_are_up_to_date());
    const Generator_System& gs = ph.generators();
    Grid_Generator_System ggs(space_dim);
    Linear_Expression point_expr;
    PPL_DIRTY_TEMP_COEFFICIENT(point_divisor);
    for (Generator_System::const_iterator g = gs.begin(),
           gs_end = gs.end(); g != gs_end; ++g) {
      if (g->is_point() || g->is_closure_point()) {
        for (dimension_type i = space_dim; i-- > 0; ) {
          const Variable v(i);
          point_expr += g->coefficient(v) * v;
          point_divisor = g->divisor();
        }
        ggs.insert(grid_point(point_expr, point_divisor));
        break;
      }
    }
    // Add grid lines for all the other generators.
    // If the polyhedron's generator is a (closure) point, the grid line must
    // have the direction given by a line that joins the grid point already
    // inserted and the new point.
    PPL_DIRTY_TEMP_COEFFICIENT(coeff);
    PPL_DIRTY_TEMP_COEFFICIENT(g_divisor);
    for (Generator_System::const_iterator g = gs.begin(),
           gs_end = gs.end(); g != gs_end; ++g) {
      Linear_Expression e;
      if (g->is_point() || g->is_closure_point()) {
        g_divisor = g->divisor();
        for (dimension_type i = space_dim; i-- > 0; ) {
          const Variable v(i);
          coeff = point_expr.coefficient(v) * g_divisor;
          coeff -= g->coefficient(v) * point_divisor;
          e += coeff * v;
        }
        if (e.all_homogeneous_terms_are_zero())
          continue;
      }
      else
        for (dimension_type i = space_dim; i-- > 0; ) {
          const Variable v(i);
          e += g->coefficient(v) * v;
        }
      ggs.insert(grid_line(e));
    }
    construct(ggs);
  }
  PPL_ASSERT(OK());
}

Parma_Polyhedra_Library::Grid::Grid	(	const Grid &	y,
		Complexity_Class	complexity = `ANY_COMPLEXITY`
	)

Ordinary copy constructor.

The complexity argument is ignored.

Definition at line 37 of file Grid_public.cc.

References con_sys, congruences_are_up_to_date(), gen_sys, generators_are_up_to_date(), Parma_Polyhedra_Library::Congruence_System::increase_space_dimension(), and space_dim.

  : con_sys(),
    gen_sys(),
    status(y.status),
    space_dim(y.space_dim),
    dim_kinds(y.dim_kinds) {
  if (space_dim == 0) {
    con_sys = y.con_sys;
    gen_sys = y.gen_sys;
  }
  else {
    if (y.congruences_are_up_to_date())
      con_sys = y.con_sys;
    else
      con_sys.increase_space_dimension(space_dim);
    if (y.generators_are_up_to_date())
      gen_sys = y.gen_sys;
    else
      gen_sys = Grid_Generator_System(y.space_dim);
  }
}

Parma_Polyhedra_Library::Grid::~Grid ( )

inline

Destructor.

Definition at line 220 of file Grid.inlines.hh.

{
}

Member Function Documentation

void Parma_Polyhedra_Library::Grid::add_congruence ( const Congruence & cg )

inline

Adds a copy of congruence cg to *this.

Exceptions:

std::invalid_argument Thrown if *this and congruence cg are dimension-incompatible.

Definition at line 259 of file Grid.inlines.hh.

References add_congruence_no_check(), marked_empty(), space_dim, Parma_Polyhedra_Library::Congruence::space_dimension(), and throw_dimension_incompatible().

Referenced by Parma_Polyhedra_Library::Affine_Space::add_congruence(), Parma_Polyhedra_Library::Pointset_Powerset< PSET >::approximate_partition_aux(), refine_with_congruence(), and simplify_using_context_assign().

                                         {
  // Dimension-compatibility check.
  if (space_dim < cg.space_dimension())
    throw_dimension_incompatible("add_congruence(cg)", "cg", cg);

  if (!marked_empty())
    add_congruence_no_check(cg);
}

void Parma_Polyhedra_Library::Grid::add_congruence_no_check ( const Congruence & cg )

private

Adds the congruence cg to *this.

Warning:: If cg and *this are dimension-incompatible, the grid generator system is not minimized or *this is empty, then the behavior is undefined.

Definition at line 646 of file Grid_nonpublic.cc.

References Parma_Polyhedra_Library::Congruence::is_inconsistent(), PPL_ASSERT, and Parma_Polyhedra_Library::Congruence::space_dimension().

Referenced by add_congruence(), and difference_assign().

                                                     {
  PPL_ASSERT(!marked_empty());
  PPL_ASSERT(space_dim >= cg.space_dimension());

  // Dealing with a zero-dimensional space grid first.
  if (space_dim == 0) {
    if (cg.is_inconsistent())
      set_empty();
    return;
  }

  if (!congruences_are_up_to_date())
    update_congruences();

  con_sys.insert(cg);

  clear_congruences_minimized();
  set_congruences_up_to_date();
  clear_generators_up_to_date();

  // Note: the congruence system may have become unsatisfiable, thus
  // we do not check for satisfiability.
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::add_congruences ( const Congruence_System & cgs )

inline

Adds a copy of each congruence in cgs to *this.

Parameters:

cgs	Contains the congruences that will be added to the system of congruences of `*this`.

Exceptions:

std::invalid_argument Thrown if *this and cgs are dimension-incompatible.

Definition at line 269 of file Grid.inlines.hh.

References add_recycled_congruences(), marked_empty(), space_dim, Parma_Polyhedra_Library::Congruence_System::space_dimension(), and throw_dimension_incompatible().

Referenced by Parma_Polyhedra_Library::Affine_Space::add_congruences(), refine_with_congruences(), and simplify_using_context_assign().

                                                  {
  // TODO: this is just an executable specification.
  // Space dimension compatibility check.
  if (space_dim < cgs.space_dimension())
    throw_dimension_incompatible("add_congruences(cgs)", "cgs", cgs);

  if (!marked_empty()) {
    Congruence_System cgs_copy = cgs;
    add_recycled_congruences(cgs_copy);
  }
}

void Parma_Polyhedra_Library::Grid::add_constraint ( const Constraint & c )

inline

Adds to *this a congruence equivalent to constraint c.

Parameters:

c	The constraint to be added.

Exceptions:

std::invalid_argument Thrown if *this and c are dimension-incompatible or if constraint c is not optimally supported by the grid domain.

Definition at line 302 of file Grid.inlines.hh.

References add_constraint_no_check(), marked_empty(), space_dim, Parma_Polyhedra_Library::Constraint::space_dimension(), and throw_dimension_incompatible().

Referenced by Parma_Polyhedra_Library::Affine_Space::add_constraint().

                                        {
  // Space dimension compatibility check.
  if (space_dim < c.space_dimension())
    throw_dimension_incompatible("add_constraint(c)", "c", c);
  if (!marked_empty())
    add_constraint_no_check(c);
}

void Parma_Polyhedra_Library::Grid::add_constraint_no_check ( const Constraint & c )

private

Uses the constraint c to refine *this.

Parameters:

c	The constraint to be added.

Exceptions:

std::invalid_argument Thrown if c is a non-trivial inequality constraint.

Warning:: If c and *this are dimension-incompatible, the behavior is undefined.

Definition at line 672 of file Grid_nonpublic.cc.

References Parma_Polyhedra_Library::Constraint::is_equality(), Parma_Polyhedra_Library::Constraint::is_inconsistent(), Parma_Polyhedra_Library::Constraint::is_inequality(), Parma_Polyhedra_Library::Constraint::is_tautological(), PPL_ASSERT, and Parma_Polyhedra_Library::Constraint::space_dimension().

Referenced by add_constraint().

                                                    {
  PPL_ASSERT(!marked_empty());
  PPL_ASSERT(space_dim >= c.space_dimension());

  if (c.is_inequality()) {
    // Only trivial inequalities can be handled.
    if (c.is_inconsistent()) {
      set_empty();
      return;
    }
    if (c.is_tautological())
      return;
    // Non-trivial inequality constraints are not allowed.
    throw_invalid_constraint("add_constraint(c)", "c");
  }

  PPL_ASSERT(c.is_equality());
  Congruence cg(c);
  add_congruence_no_check(cg);
}

void Parma_Polyhedra_Library::Grid::add_constraints ( const Constraint_System & cs )

Adds to *this congruences equivalent to the constraints in cs.

Parameters:

cs	The constraints to be added.

Exceptions:

std::invalid_argument Thrown if *this and cs are dimension-incompatible or if cs contains a constraint which is not optimally supported by the grid domain.

Definition at line 1148 of file Grid_public.cc.

References Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Constraint_System::end(), and Parma_Polyhedra_Library::Constraint_System::space_dimension().

Referenced by add_recycled_constraints().

                                                    {
  // The dimension of `cs' must be at most `space_dim'.
  if (space_dim < cs.space_dimension())
    throw_dimension_incompatible("add_constraints(cs)", "cs", cs);
  if (marked_empty())
    return;

  for (Constraint_System::const_iterator i = cs.begin(),
         cs_end = cs.end(); i != cs_end; ++i) {
    add_constraint_no_check(*i);
    if (marked_empty())
      return;
  }
}

void Parma_Polyhedra_Library::Grid::add_grid_generator ( const Grid_Generator & g )

Adds a copy of grid generator g to the system of generators of *this.

Exceptions:

std::invalid_argument Thrown if *this and generator g are dimension-incompatible, or if *this is an empty grid and g is not a point.

Definition at line 1164 of file Grid_public.cc.

References Parma_Polyhedra_Library::Grid_Generator::is_line_or_parameter(), Parma_Polyhedra_Library::Grid_Generator::is_parameter(), Parma_Polyhedra_Library::Grid_Generator::is_parameter_or_point(), PPL_ASSERT, and Parma_Polyhedra_Library::Grid_Generator::space_dimension().

                                                   {
  // The dimension of `g' must be at most space_dim.
  const dimension_type g_space_dim = g.space_dimension();
  if (space_dim < g_space_dim)
    throw_dimension_incompatible("add_grid_generator(g)", "g", g);

  // Deal with zero-dimension case first.
  if (space_dim == 0) {
    // Points and parameters are the only zero-dimension generators
    // that can be created.
    if (marked_empty()) {
      if (g.is_parameter())
        throw_invalid_generator("add_grid_generator(g)", "g");
      set_zero_dim_univ();
    }
    PPL_ASSERT(OK());
    return;
  }

  if (marked_empty()
      || (!generators_are_up_to_date() && !update_generators())) {
    // Here the grid is empty: the specification says we can only
    // insert a point.
    if (g.is_line_or_parameter())
      throw_invalid_generator("add_grid_generator(g)", "g");
    gen_sys.insert(g);
    clear_empty();
  }
  else {
    PPL_ASSERT(generators_are_up_to_date());
    gen_sys.insert(g);
    if (g.is_parameter_or_point())
      normalize_divisors(gen_sys);
  }

  // With the added generator, congruences are out of date.
  clear_congruences_up_to_date();

  clear_generators_minimized();
  set_generators_up_to_date();
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::add_grid_generators ( const Grid_Generator_System & gs )

Adds a copy of the generators in gs to the system of generators of *this.

Parameters:

gs	Contains the generators that will be added to the system of generators of `*this`.

Exceptions:

std::invalid_argument Thrown if *this and gs are dimension-incompatible, or if *this is empty and the system of generators gs is not empty, but has no points.

Definition at line 1308 of file Grid_public.cc.

                                                            {
  // TODO: this is just an executable specification.
  Grid_Generator_System gs_copy = gs;
  add_recycled_grid_generators(gs_copy);
}

void Parma_Polyhedra_Library::Grid::add_recycled_congruences ( Congruence_System & cgs )

Adds the congruences in cgs to *this.

Parameters:

cgs	The congruence system to be added to `*this`. The congruences in `cgs` may be recycled.

Exceptions:

std::invalid_argument Thrown if *this and cgs are dimension-incompatible.

Warning:: The only assumption that can be made about cgs upon successful or exceptional return is that it can be safely destroyed.

Definition at line 1208 of file Grid_public.cc.

References Parma_Polyhedra_Library::Congruence_System::begin(), Parma_Polyhedra_Library::Congruence_System::end(), Parma_Polyhedra_Library::Dense_Matrix::has_no_rows(), PPL_ASSERT, and Parma_Polyhedra_Library::Congruence_System::space_dimension().

Referenced by add_congruences(), congruence_widening_assign(), contains_integer_point(), limited_congruence_extrapolation_assign(), limited_extrapolation_assign(), limited_generator_extrapolation_assign(), and simplify_using_context_assign().

                                                        {
  // Dimension-compatibility check.
  const dimension_type cgs_space_dim = cgs.space_dimension();
  if (space_dim < cgs_space_dim)
    throw_dimension_incompatible("add_recycled_congruences(cgs)", "cgs", cgs);

  if (cgs.has_no_rows())
    return;

  if (marked_empty())
    return;

  if (space_dim == 0) {
    // In a 0-dimensional space the congruences are trivial (e.g., 0
    // == 0 or 1 %= 0) or false (e.g., 1 == 0).  In a system of
    // congruences `begin()' and `end()' are equal if and only if the
    // system contains only trivial congruences.
    if (cgs.begin() != cgs.end())
      // There is a congruence, it must be false, the grid becomes empty.
      set_empty();
    return;
  }

  // The congruences are required.
  if (!congruences_are_up_to_date())
    update_congruences();

  // Swap (instead of copying) the coefficients of `cgs' (which is
  // writable).
  con_sys.recycling_insert(cgs);

  // Congruences may not be minimized and generators are out of date.
  clear_congruences_minimized();
  clear_generators_up_to_date();
  // Note: the congruence system may have become unsatisfiable, thus
  // we do not check for satisfiability.
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::add_recycled_constraints ( Constraint_System & cs )

inline

Adds to *this congruences equivalent to the constraints in cs.

Parameters:

cs	The constraints to be added. They may be recycled.

Exceptions:

std::invalid_argument Thrown if *this and cs are dimension-incompatible or if cs contains a constraint which is not optimally supported by the grid domain.

Warning:: The only assumption that can be made about cs upon successful or exceptional return is that it can be safely destroyed.

Definition at line 311 of file Grid.inlines.hh.

References add_constraints().

Referenced by Parma_Polyhedra_Library::Affine_Space::add_recycled_constraints().

                                                    {
  // TODO: really recycle the constraints.
  add_constraints(cs);
}

void Parma_Polyhedra_Library::Grid::add_recycled_grid_generators ( Grid_Generator_System & gs )

Adds the generators in gs to the system of generators of *this.

Parameters:

gs	The generator system to be added to `*this`. The generators in `gs` may be recycled.

Exceptions:

std::invalid_argument Thrown if *this and gs are dimension-incompatible.

Warning:: The only assumption that can be made about gs upon successful or exceptional return is that it can be safely destroyed.

Definition at line 1248 of file Grid_public.cc.

References Parma_Polyhedra_Library::Dense_Matrix::has_no_rows(), Parma_Polyhedra_Library::Grid_Generator_System::has_points(), Parma_Polyhedra_Library::Grid_Generator_System::insert(), PPL_ASSERT, and Parma_Polyhedra_Library::Grid_Generator_System::space_dimension().

Referenced by generator_widening_assign().

                                                               {
  // Dimension-compatibility check.
  const dimension_type gs_space_dim = gs.space_dimension();
  if (space_dim < gs_space_dim)
    throw_dimension_incompatible("add_recycled_grid_generators(gs)", "gs", gs);

  // Adding no generators leaves the grid the same.
  if (gs.has_no_rows())
    return;

  // Adding valid generators to a zero-dimensional grid transforms it
  // to the zero-dimensional universe grid.
  if (space_dim == 0) {
    if (marked_empty())
      set_zero_dim_univ();
    else {
      PPL_ASSERT(gs.has_points());
    }
    PPL_ASSERT(OK(true));
    return;
  }

  if (!marked_empty()) {
    // The grid contains at least one point.

    if (!generators_are_up_to_date())
      update_generators();
    normalize_divisors(gs, gen_sys);

    gen_sys.recycling_insert(gs);

    // Congruences are out of date and generators are not minimized.
    clear_congruences_up_to_date();
    clear_generators_minimized();

    PPL_ASSERT(OK(true));
    return;
  }

  // The grid is empty.

  // `gs' must contain at least one point.
  if (!gs.has_points())
    throw_invalid_generators("add_recycled_grid_generators(gs)", "gs");

  // Adjust `gs' to the right dimension.
  gs.insert(parameter(0*Variable(space_dim-1)));

  gen_sys.m_swap(gs);

  normalize_divisors(gen_sys);

  // The grid is no longer empty and generators are up-to-date.
  set_generators_up_to_date();
  clear_empty();

  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::add_space_dimensions	(	Congruence_System &	cgs,
		Grid_Generator_System &	gs,
		dimension_type	dims
	)

private

Adds new space dimensions to the given systems.

Parameters:

cgs	A congruence system, to which columns are added;
gs	A generator system, to which rows and columns are added;
dims	The number of space dimensions to add.

This method is invoked only by add_space_dimensions_and_embed().

Definition at line 34 of file Grid_chdims.cc.

References Parma_Polyhedra_Library::Grid_Generator_System::add_universe_rows_and_columns(), Parma_Polyhedra_Library::Dense_Matrix::add_zero_columns(), CON_VIRTUAL, congruences_are_minimized(), dim_kinds, generators_are_minimized(), Parma_Polyhedra_Library::Dense_Matrix::num_columns(), PPL_ASSERT, Parma_Polyhedra_Library::Grid_Generator_System::space_dimension(), and Parma_Polyhedra_Library::Dense_Matrix::swap_columns().

                                                           {
  PPL_ASSERT(cgs.num_columns() - 1 == gs.space_dimension() + 1);
  PPL_ASSERT(dims > 0);

  const dimension_type old_modulus_index = cgs.num_columns() - 1;
  cgs.add_zero_columns(dims);
  // Move the moduli.
  cgs.swap_columns(old_modulus_index, old_modulus_index + dims);

  if (congruences_are_minimized() || generators_are_minimized())
    dim_kinds.resize(old_modulus_index + dims, CON_VIRTUAL /* a.k.a. LINE */);

  gs.add_universe_rows_and_columns(dims);
}

void Parma_Polyhedra_Library::Grid::add_space_dimensions	(	Grid_Generator_System &	gs,
		Congruence_System &	cgs,
		dimension_type	dims
	)

private

Adds new space dimensions to the given systems.

Parameters:

gs	A generator system, to which columns are added;
cgs	A congruence system, to which rows and columns are added;
dims	The number of space dimensions to add.

This method is invoked only by add_space_dimensions_and_project().

Definition at line 53 of file Grid_chdims.cc.

References Parma_Polyhedra_Library::Congruence_System::add_unit_rows_and_columns(), Parma_Polyhedra_Library::Grid_Generator_System::insert(), Parma_Polyhedra_Library::Dense_Matrix::num_columns(), PPL_ASSERT, and Parma_Polyhedra_Library::Grid_Generator_System::space_dimension().

                                                           {
  PPL_ASSERT(cgs.num_columns() - 1 == gs.space_dimension() + 1);
  PPL_ASSERT(dims > 0);

  cgs.add_unit_rows_and_columns(dims);

  // Add `dims' zero columns onto gs.
  gs.insert(parameter(0*Variable(space_dim + dims - 1)));

  normalize_divisors(gs);

  dim_kinds.resize(cgs.num_columns() - 1, EQUALITY /* a.k.a GEN_VIRTUAL */);
}

void Parma_Polyhedra_Library::Grid::add_space_dimensions_and_embed ( dimension_type m )

Adds m new space dimensions and embeds the old grid in the new vector space.

Parameters:

m	The number of dimensions to add.

Exceptions:

std::length_error Thrown if adding m new space dimensions would cause the vector space to exceed dimension max_space_dimension().

The new space dimensions will be those having the highest indexes in the new grid, which is characterized by a system of congruences in which the variables which are the new dimensions can have any value. For instance, when starting from the grid $\cL \sseq \Rset^2$ and adding a third space dimension, the result will be the grid

$\bigl\{\, (x, y, z)^\transpose \in \Rset^3 \bigm| (x, y)^\transpose \in \cL \,\bigr\}.$

Definition at line 78 of file Grid_chdims.cc.

References Parma_Polyhedra_Library::check_space_dimension_overflow(), Parma_Polyhedra_Library::max_space_dimension(), PPL_ASSERT, and Parma_Polyhedra_Library::UNIVERSE.

Referenced by simplify_using_context_assign().

                                                        {
  if (m == 0)
    return;

  // The space dimension of the resulting grid must be at most the
  // maximum allowed space dimension.
  check_space_dimension_overflow(m, max_space_dimension() - space_dimension(),
                                 "PPL::Grid::",
                                 "add_space_dimensions_and_embed(m)",
                                 "adding m new space dimensions exceeds "
                                 "the maximum allowed space dimension");

  // Adding dimensions to an empty grid is obtained by adjusting
  // `space_dim' and clearing `con_sys' (since it can contain the
  // integrality congruence of the current dimension).
  if (marked_empty()) {
    space_dim += m;
    set_empty();
    return;
  }

  // The case of a zero-dimension space grid.
  if (space_dim == 0) {
    // Since it is not empty, it has to be the universe grid.
    PPL_ASSERT(status.test_zero_dim_univ());
    // Swap *this with a newly created `m'-dimensional universe grid.
    Grid gr(m, UNIVERSE);
    m_swap(gr);
    return;
  }

  // To embed an n-dimension space grid in a (n+m)-dimension space, we
  // add `m' zero-columns to the rows in the system of congruences; in
  // contrast, the system of generators needs additional rows,
  // corresponding to the vectors of the canonical basis for the added
  // dimensions. That is, for each new dimension we add the line
  // having that direction. This is done by invoking the function
  // add_space_dimensions().
  if (congruences_are_up_to_date())
    if (generators_are_up_to_date())
      // Adds rows and/or columns to both matrices.
      add_space_dimensions(con_sys, gen_sys, m);
    else {
      // Only congruences are up-to-date, so modify only them.
      con_sys.add_zero_columns(m);
      dimension_type size = con_sys.num_columns() - 1;
      // Move the moduli.
      con_sys.swap_columns(size - m, size);
      if (congruences_are_minimized())
        dim_kinds.resize(size, CON_VIRTUAL);
    }
  else {
    // Only generators are up-to-date, so modify only them.
    PPL_ASSERT(generators_are_up_to_date());
    gen_sys.add_universe_rows_and_columns(m);
    if (generators_are_minimized())
      dim_kinds.resize(gen_sys.space_dimension() + 1, LINE);
  }
  // Update the space dimension.
  space_dim += m;

  // Note: we do not check for satisfiability, because the system of
  // congruences may be unsatisfiable.
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::add_space_dimensions_and_project ( dimension_type m )

Adds m new space dimensions to the grid and does not embed it in the new vector space.

Parameters:

m	The number of space dimensions to add.

Exceptions:

std::length_error Thrown if adding m new space dimensions would cause the vector space to exceed dimension max_space_dimension().

The new space dimensions will be those having the highest indexes in the new grid, which is characterized by a system of congruences in which the variables running through the new dimensions are all constrained to be equal to 0. For instance, when starting from the grid $\cL \sseq \Rset^2$ and adding a third space dimension, the result will be the grid

$\bigl\{\, (x, y, 0)^\transpose \in \Rset^3 \bigm| (x, y)^\transpose \in \cL \,\bigr\}.$

Definition at line 153 of file Grid_chdims.cc.

References Parma_Polyhedra_Library::check_space_dimension_overflow(), Parma_Polyhedra_Library::max_space_dimension(), PPL_ASSERT, and Parma_Polyhedra_Library::UNIVERSE.

                                                          {
  if (m == 0)
    return;

  // The space dimension of the resulting grid should be at most the
  // maximum allowed space dimension.
  check_space_dimension_overflow(m, max_space_dimension() - space_dimension(),
                                 "PPL::Grid::",
                                 "add_space_dimensions_and_project(m)",
                                 "adding m new space dimensions exceeds "
                                 "the maximum allowed space dimension");

  // Adding dimensions to an empty grid is obtained by merely
  // adjusting `space_dim'.
  if (marked_empty()) {
    space_dim += m;
    set_empty();
    return;
  }

  if (space_dim == 0) {
    PPL_ASSERT(status.test_zero_dim_univ());
    // Swap *this with a newly created `n'-dimensional universe grid.
    Grid gr(m, UNIVERSE);
    m_swap(gr);
    return;
  }

  // To project an n-dimension space grid in a (n+m)-dimension space,
  // we just add to the system of generators `m' zero-columns; in
  // contrast, in the system of congruences, new rows are needed in
  // order to avoid embedding the old grid in the new space.  Thus,
  // for each new dimensions `x[k]', we add the constraint x[k] = 0;
  // this is done by invoking the function add_space_dimensions()
  // giving the system of constraints as the second argument.
  if (congruences_are_up_to_date())
    if (generators_are_up_to_date())
      // Add rows and/or columns to both matrices.
      add_space_dimensions(gen_sys, con_sys, m);
    else {
      // Only congruences are up-to-date so modify only them.
      con_sys.add_unit_rows_and_columns(m);
      if (congruences_are_minimized())
        dim_kinds.resize(con_sys.num_columns() - 1, EQUALITY);
    }
  else {
    // Only generators are up-to-date so modify only them.
    PPL_ASSERT(generators_are_up_to_date());

    // Add m zero columns onto gs.
    gen_sys.insert(parameter(0*Variable(space_dim + m - 1)));

    normalize_divisors(gen_sys);

    if (generators_are_minimized())
      dim_kinds.resize(gen_sys.space_dimension() + 1, EQUALITY);
  }
  // Now update the space dimension.
  space_dim += m;

  // Note: we do not check for satisfiability, because the system of
  // congruences may be unsatisfiable.
  PPL_ASSERT(OK());
}

PPL::dimension_type Parma_Polyhedra_Library::Grid::affine_dimension ( ) const

Returns $0$ , if *this is empty; otherwise, returns the affine dimension of *this.

Definition at line 260 of file Grid_public.cc.

References PPL_ASSERT.

                                {
  if (space_dim == 0 || is_empty())
    return 0;

  if (generators_are_up_to_date()) {
    if (generators_are_minimized())
      return gen_sys.num_rows() - 1;
    if (!(congruences_are_up_to_date() && congruences_are_minimized()))
      return minimized_grid_generators().num_rows() - 1;
  }
  else
    minimized_congruences();
  PPL_ASSERT(congruences_are_minimized());
  dimension_type d = space_dim;
  for (dimension_type i = con_sys.num_rows(); i-- > 0; )
    if (con_sys[i].is_equality())
      --d;
  return d;
}

void Parma_Polyhedra_Library::Grid::affine_image	(	Variable	var,
		const Linear_Expression &	expr,
		Coefficient_traits::const_reference	denominator = `Coefficient_one()`
	)

Assigns to *this the affine image of *this under the function mapping variable var to the affine expression specified by expr and denominator.

Parameters:

var	The variable to which the affine expression is assigned;
expr	The numerator of the affine expression;
denominator	The denominator of the affine expression (optional argument with default value 1).

Exceptions:

std::invalid_argument Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a space dimension of *this.

When considering the generators of a grid, the affine transformation

$\frac{\sum_{i=0}^{n-1} a_i x_i + b}{\mathrm{denominator}}$

is assigned to var where expr is $\sum_{i=0}^{n-1} a_i x_i + b$ ( $b$ is the inhomogeneous term).

If congruences are up-to-date, it uses the specialized function affine_preimage() (for the system of congruences) and inverse transformation to reach the same result. To obtain the inverse transformation we use the following observation.

Observation:

The affine transformation is invertible if the coefficient of var in this transformation (i.e., $a_\mathrm{var}$ ) is different from zero.
If the transformation is invertible, then we can write
$\mathrm{denominator} * {x'}_\mathrm{var} = \sum_{i = 0}^{n - 1} a_i x_i + b = a_\mathrm{var} x_\mathrm{var} + \sum_{i \neq var} a_i x_i + b,$
so that the inverse transformation is
$a_\mathrm{var} x_\mathrm{var} = \mathrm{denominator} * {x'}_\mathrm{var} - \sum_{i \neq j} a_i x_i - b.$

Then, if the transformation is invertible, all the entities that were up-to-date remain up-to-date. Otherwise only generators remain up-to-date.

Definition at line 1775 of file Grid_public.cc.

References Parma_Polyhedra_Library::inverse(), Parma_Polyhedra_Library::neg_assign(), PPL_ASSERT, Parma_Polyhedra_Library::Variable::space_dimension(), and Parma_Polyhedra_Library::Linear_Expression::space_dimension().

Referenced by fold_space_dimensions().

                                                                       {
  // The denominator cannot be zero.
  if (denominator == 0)
    throw_invalid_argument("affine_image(v, e, d)", "d == 0");

  // Dimension-compatibility checks.
  // The dimension of `expr' must be at most the dimension of `*this'.
  const dimension_type expr_space_dim = expr.space_dimension();
  if (space_dim < expr_space_dim)
    throw_dimension_incompatible("affine_image(v, e, d)", "e", expr);
  // `var' must be one of the dimensions of the grid.
  const dimension_type var_space_dim = var.space_dimension();
  if (space_dim < var_space_dim)
    throw_dimension_incompatible("affine_image(v, e, d)", "v", var);

  if (marked_empty())
    return;

  if (var_space_dim <= expr_space_dim && expr[var_space_dim] != 0) {
    // The transformation is invertible.
    if (generators_are_up_to_date()) {
      // Grid_Generator_System::affine_image() requires the third argument
      // to be a positive Coefficient.
      if (denominator > 0)
        gen_sys.affine_image(var_space_dim, expr, denominator);
      else
        gen_sys.affine_image(var_space_dim, -expr, -denominator);
      clear_generators_minimized();
      // Strong normalization in gs::affine_image may have modified
      // divisors.
      normalize_divisors(gen_sys);
    }
    if (congruences_are_up_to_date()) {
      // To build the inverse transformation,
      // after copying and negating `expr',
      // we exchange the roles of `expr[var_space_dim]' and `denominator'.
      Linear_Expression inverse;
      if (expr[var_space_dim] > 0) {
        inverse = -expr;
        inverse[var_space_dim] = denominator;
        con_sys.affine_preimage(var_space_dim, inverse, expr[var_space_dim]);
      }
      else {
        // The new denominator is negative: we negate everything once
        // more, as Congruence_System::affine_preimage() requires the
        // third argument to be positive.
        inverse = expr;
        inverse[var_space_dim] = denominator;
        neg_assign(inverse[var_space_dim]);
        con_sys.affine_preimage(var_space_dim, inverse, -expr[var_space_dim]);
      }
      clear_congruences_minimized();
    }
  }
  else {
    // The transformation is not invertible.
    // We need an up-to-date system of generators.
    if (!generators_are_up_to_date())
      minimize();
    if (!marked_empty()) {
      // Grid_Generator_System::affine_image() requires the third argument
      // to be a positive Coefficient.
      if (denominator > 0)
        gen_sys.affine_image(var_space_dim, expr, denominator);
      else
        gen_sys.affine_image(var_space_dim, -expr, -denominator);

      clear_congruences_up_to_date();
      clear_generators_minimized();
      // Strong normalization in gs::affine_image may have modified
      // divisors.
      normalize_divisors(gen_sys);
    }
  }
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::affine_preimage	(	Variable	var,
		const Linear_Expression &	expr,
		Coefficient_traits::const_reference	denominator = `Coefficient_one()`
	)

Assigns to *this the affine preimage of *this under the function mapping variable var to the affine expression specified by expr and denominator.

Parameters:

var	The variable to which the affine expression is substituted;
expr	The numerator of the affine expression;
denominator	The denominator of the affine expression (optional argument with default value 1).

Exceptions:

std::invalid_argument Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a space dimension of *this.

When considering congruences of a grid, the affine transformation

$\frac{\sum_{i=0}^{n-1} a_i x_i + b}{denominator},$

is assigned to var where expr is $\sum_{i=0}^{n-1} a_i x_i + b$ ( $b$ is the inhomogeneous term).

If generators are up-to-date, then the specialized function affine_image() is used (for the system of generators) and inverse transformation to reach the same result. To obtain the inverse transformation, we use the following observation.

Observation:

The affine transformation is invertible if the coefficient of var in this transformation (i.e. $a_\mathrm{var}$ ) is different from zero.
If the transformation is invertible, then we can write
$\mathrm{denominator} * {x'}_\mathrm{var} = \sum_{i = 0}^{n - 1} a_i x_i + b = a_\mathrm{var} x_\mathrm{var} + \sum_{i \neq \mathrm{var}} a_i x_i + b,$
, the inverse transformation is
$a_\mathrm{var} x_\mathrm{var} = \mathrm{denominator} * {x'}_\mathrm{var} - \sum_{i \neq j} a_i x_i - b.$
.

Then, if the transformation is invertible, all the entities that were up-to-date remain up-to-date. Otherwise only congruences remain up-to-date.

Definition at line 1856 of file Grid_public.cc.

References Parma_Polyhedra_Library::inverse(), Parma_Polyhedra_Library::neg_assign(), PPL_ASSERT, Parma_Polyhedra_Library::Variable::space_dimension(), and Parma_Polyhedra_Library::Linear_Expression::space_dimension().

                                                               {
  // The denominator cannot be zero.
  if (denominator == 0)
    throw_invalid_argument("affine_preimage(v, e, d)", "d == 0");

  // Dimension-compatibility checks.
  // The dimension of `expr' should not be greater than the dimension
  // of `*this'.
  const dimension_type expr_space_dim = expr.space_dimension();
  if (space_dim < expr_space_dim)
    throw_dimension_incompatible("affine_preimage(v, e, d)", "e", expr);
  // `var' should be one of the dimensions of the grid.
  const dimension_type var_space_dim = var.space_dimension();
  if (space_dim < var_space_dim)
    throw_dimension_incompatible("affine_preimage(v, e, d)", "v", var);

  if (marked_empty())
    return;

  if (var_space_dim <= expr_space_dim && expr[var_space_dim] != 0) {
    // The transformation is invertible.
    if (congruences_are_up_to_date()) {
      // Congruence_System::affine_preimage() requires the third argument
      // to be a positive Coefficient.
      if (denominator > 0)
        con_sys.affine_preimage(var_space_dim, expr, denominator);
      else
        con_sys.affine_preimage(var_space_dim, -expr, -denominator);
      clear_congruences_minimized();
    }
    if (generators_are_up_to_date()) {
      // To build the inverse transformation,
      // after copying and negating `expr',
      // we exchange the roles of `expr[var_space_dim]' and `denominator'.
      Linear_Expression inverse;
      if (expr[var_space_dim] > 0) {
        inverse = -expr;
        inverse[var_space_dim] = denominator;
        gen_sys.affine_image(var_space_dim, inverse, expr[var_space_dim]);
      }
      else {
        // The new denominator is negative: we negate everything once
        // more, as Grid_Generator_System::affine_image() requires the
        // third argument to be positive.
        inverse = expr;
        inverse[var_space_dim] = denominator;
        neg_assign(inverse[var_space_dim]);
        gen_sys.affine_image(var_space_dim, inverse, -expr[var_space_dim]);
      }
      clear_generators_minimized();
    }
  }
  else {
    // The transformation is not invertible.
    // We need an up-to-date system of congruences.
    if (!congruences_are_up_to_date())
      minimize();
    // Congruence_System::affine_preimage() requires the third argument
    // to be a positive Coefficient.
    if (denominator > 0)
      con_sys.affine_preimage(var_space_dim, expr, denominator);
    else
      con_sys.affine_preimage(var_space_dim, -expr, -denominator);

    clear_generators_up_to_date();
    clear_congruences_minimized();
  }
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::ascii_dump ( ) const

Writes to std::cerr an ASCII representation of *this.

void Parma_Polyhedra_Library::Grid::ascii_dump ( std::ostream & s ) const

Writes to s an ASCII representation of *this.

Definition at line 2604 of file Grid_public.cc.

                                       {
  using std::endl;

  s << "space_dim "
    << space_dim
    << endl;
  status.ascii_dump(s);
  s << "con_sys ("
    << (congruences_are_up_to_date() ? "" : "not_")
    << "up-to-date)"
    << endl;
  con_sys.ascii_dump(s);
  s << "gen_sys ("
    << (generators_are_up_to_date() ? "" : "not_")
    << "up-to-date)"
    << endl;
  gen_sys.ascii_dump(s);
  s << "dimension_kinds";
  if ((generators_are_up_to_date() && generators_are_minimized())
      || (congruences_are_up_to_date() && congruences_are_minimized()))
    for (Dimension_Kinds::const_iterator i = dim_kinds.begin();
         i != dim_kinds.end();
         ++i)
      s << " " << *i;
  s << endl;
}

bool Parma_Polyhedra_Library::Grid::ascii_load ( std::istream & s )

Loads from s an ASCII representation (as produced by ascii_dump(std::ostream&) const) and sets *this accordingly. Returns true if successful, false otherwise.

Definition at line 2634 of file Grid_public.cc.

References PPL_ASSERT.

                                 {
  std::string str;

  if (!(s >> str) || str != "space_dim")
    return false;

  if (!(s >> space_dim))
    return false;

  if (!status.ascii_load(s))
    return false;

  if (!(s >> str) || str != "con_sys")
    return false;

  if (!(s >> str))
    return false;
  if (str == "(up-to-date)")
    set_congruences_up_to_date();
  else if (str != "(not_up-to-date)")
    return false;

  if (!con_sys.ascii_load(s))
    return false;

  if (!(s >> str) || str != "gen_sys")
    return false;

  if (!(s >> str))
    return false;
  if (str == "(up-to-date)")
    set_generators_up_to_date();
  else if (str != "(not_up-to-date)")
    return false;

  if (!gen_sys.ascii_load(s))
    return false;

  if (!(s >> str) || str != "dimension_kinds")
    return false;

  if (!marked_empty()
      && ((generators_are_up_to_date() && generators_are_minimized())
          || (congruences_are_up_to_date() && congruences_are_minimized()))) {
    dim_kinds.resize(space_dim + 1);
    for (Dimension_Kinds::size_type dim = 0; dim <= space_dim; ++dim) {
      short unsigned int dim_kind;
      if (!(s >> dim_kind))
        return false;
      switch(dim_kind) {
      case 0: dim_kinds[dim] = PARAMETER; break;
      case 1: dim_kinds[dim] = LINE; break;
      case 2: dim_kinds[dim] = GEN_VIRTUAL; break;
      default: return false;
      }
    }
  }

  // Check invariants.
  PPL_ASSERT(OK());
  return true;
}

void Parma_Polyhedra_Library::Grid::bounded_affine_image	(	Variable	var,
		const Linear_Expression &	lb_expr,
		const Linear_Expression &	ub_expr,
		Coefficient_traits::const_reference	denominator = `Coefficient_one()`
	)

Assigns to *this the image of *this with respect to the bounded affine relation $\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}$ .

Parameters:

var	The variable updated by the affine relation;
lb_expr	The numerator of the lower bounding affine expression;
ub_expr	The numerator of the upper bounding affine expression;
denominator	The (common) denominator for the lower and upper bounding affine expressions (optional argument with default value 1).

Exceptions:

std::invalid_argument Thrown if denominator is zero or if lb_expr (resp., ub_expr) and *this are dimension-incompatible or if var is not a space dimension of *this.

Definition at line 2383 of file Grid_public.cc.

References Parma_Polyhedra_Library::LESS_OR_EQUAL, PPL_ASSERT, Parma_Polyhedra_Library::Variable::space_dimension(), and Parma_Polyhedra_Library::Linear_Expression::space_dimension().

                                                                    {

  // The denominator cannot be zero.
  if (denominator == 0)
    throw_invalid_argument("bounded_affine_image(v, lb, ub, d)", "d == 0");

  // Dimension-compatibility checks.
  // `var' should be one of the dimensions of the grid.
  const dimension_type var_space_dim = var.space_dimension();
  if (space_dim < var_space_dim)
    throw_dimension_incompatible("bounded_affine_image(v, lb, ub, d)",
                                 "v", var);
  // The dimension of `lb_expr' and `ub_expr' should not be
  // greater than the dimension of `*this'.
  const dimension_type lb_space_dim = lb_expr.space_dimension();
  if (space_dim < lb_space_dim)
    throw_dimension_incompatible("bounded_affine_image(v, lb, ub, d)",
                                 "lb", lb_expr);
  const dimension_type ub_space_dim = ub_expr.space_dimension();
  if (space_dim < ub_space_dim)
    throw_dimension_incompatible("bounded_affine_image(v, lb, ub, d)",
                                 "ub", ub_expr);

  // Any image of an empty grid is empty.
  if (marked_empty())
    return;

  // In all other cases, generalized_affine_preimage() must
  // just add a line in the direction of var.
  generalized_affine_image(var,
                           LESS_OR_EQUAL,
                           ub_expr,
                           denominator);

  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::bounded_affine_preimage	(	Variable	var,
		const Linear_Expression &	lb_expr,
		const Linear_Expression &	ub_expr,
		Coefficient_traits::const_reference	denominator = `Coefficient_one()`
	)

Assigns to *this the preimage of *this with respect to the bounded affine relation $\frac{\mathrm{lb\_expr}}{\mathrm{denominator}} \leq \mathrm{var}' \leq \frac{\mathrm{ub\_expr}}{\mathrm{denominator}}$ .

Parameters:

var	The variable updated by the affine relation;
lb_expr	The numerator of the lower bounding affine expression;
ub_expr	The numerator of the upper bounding affine expression;
denominator	The (common) denominator for the lower and upper bounding affine expressions (optional argument with default value 1).

Exceptions:

std::invalid_argument Thrown if denominator is zero or if lb_expr (resp., ub_expr) and *this are dimension-incompatible or if var is not a space dimension of *this.

Definition at line 2426 of file Grid_public.cc.

References Parma_Polyhedra_Library::LESS_OR_EQUAL, PPL_ASSERT, Parma_Polyhedra_Library::Variable::space_dimension(), and Parma_Polyhedra_Library::Linear_Expression::space_dimension().

                                                                       {

  // The denominator cannot be zero.
  if (denominator == 0)
    throw_invalid_argument("bounded_affine_preimage(v, lb, ub, d)", "d == 0");

  // Dimension-compatibility checks.
  // `var' should be one of the dimensions of the grid.
  const dimension_type var_space_dim = var.space_dimension();
  if (space_dim < var_space_dim)
    throw_dimension_incompatible("bounded_affine_preimage(v, lb, ub, d)",
                                 "v", var);
  // The dimension of `lb_expr' and `ub_expr' should not be
  // greater than the dimension of `*this'.
  const dimension_type lb_space_dim = lb_expr.space_dimension();
  if (space_dim < lb_space_dim)
    throw_dimension_incompatible("bounded_affine_preimage(v, lb, ub, d)",
                                 "lb", lb_expr);
  const dimension_type ub_space_dim = ub_expr.space_dimension();
  if (space_dim < ub_space_dim)
    throw_dimension_incompatible("bounded_affine_preimage(v, lb, ub, d)",
                                 "ub", ub_expr);

  // Any preimage of an empty grid is empty.
  if (marked_empty())
    return;

  // In all other cases, generalized_affine_preimage() must
  // just add a line in the direction of var.
  generalized_affine_preimage(var,
                              LESS_OR_EQUAL,
                              ub_expr,
                              denominator);

  PPL_ASSERT(OK());
}

bool Parma_Polyhedra_Library::Grid::bounds	(	const Linear_Expression &	expr,
		const char *	method_call
	)		const

private

Checks if and how expr is bounded in *this.

Returns true if and only if from_above is true and expr is bounded from above in *this, or from_above is false and expr is bounded from below in *this.

Parameters:

expr	The linear expression to test;
method_call	The call description of the public parent method, for example "bounded_from_above(e)". Passed to throw_dimension_incompatible, as the first argument.

Exceptions:

std::invalid_argument Thrown if expr and *this are dimension-incompatible.

Definition at line 274 of file Grid_nonpublic.cc.

References Parma_Polyhedra_Library::Linear_Expression::space_dimension().

Referenced by bounds_from_above(), and bounds_from_below().

                                                 {
  // The dimension of `expr' must be at most the dimension of *this.
  if (space_dim < expr.space_dimension())
    throw_dimension_incompatible(method_call, "e", expr);

  // A zero-dimensional or empty grid bounds everything.
  if (space_dim == 0
      || marked_empty()
      || (!generators_are_up_to_date() && !update_generators()))
    return true;
  if (!generators_are_minimized() && !minimize())
    // Minimizing found `this' empty.
    return true;

  return bounds_no_check(expr);
}

bool Parma_Polyhedra_Library::Grid::bounds_from_above ( const Linear_Expression & expr ) const

inline

Returns true if and only if expr is bounded in *this.

This method is the same as bounds_from_below.

Exceptions:

std::invalid_argument Thrown if expr and *this are dimension-incompatible.

Definition at line 317 of file Grid.inlines.hh.

References bounds().

Referenced by Parma_Polyhedra_Library::Affine_Space::bounds_from_above().

                                                           {
  return bounds(expr, "bounds_from_above(e)");
}

bool Parma_Polyhedra_Library::Grid::bounds_from_below ( const Linear_Expression & expr ) const

inline

Returns true if and only if expr is bounded in *this.

This method is the same as bounds_from_above.

Exceptions:

std::invalid_argument Thrown if expr and *this are dimension-incompatible.

Definition at line 322 of file Grid.inlines.hh.

References bounds().

Referenced by Parma_Polyhedra_Library::Affine_Space::bounds_from_below().

                                                           {
  return bounds(expr, "bounds_from_below(e)");
}

bool Parma_Polyhedra_Library::Grid::bounds_no_check ( const Linear_Expression & expr ) const

private

Checks if and how expr is bounded in *this.

Returns true if and only if from_above is true and expr is bounded from above in *this, or from_above is false and expr is bounded from below in *this.

Parameters:

expr	The linear expression to test;

Definition at line 293 of file Grid_nonpublic.cc.

References Parma_Polyhedra_Library::Scalar_Products::homogeneous_sign(), Parma_Polyhedra_Library::Grid_Generator::is_line_or_parameter(), PPL_ASSERT, and Parma_Polyhedra_Library::Linear_Expression::space_dimension().

Referenced by wrap_assign().

                                                            {
  // The dimension of `expr' must be at most the dimension of *this.
  PPL_ASSERT(space_dim > 0 && space_dim >= expr.space_dimension());
  PPL_ASSERT(generators_are_minimized() && !marked_empty());

  // The generators are up to date and minimized.
  for (dimension_type i = gen_sys.num_rows(); i-- > 0; ) {
    const Grid_Generator& g = gen_sys[i];
    // Only lines and parameters in `*this' can cause `expr' to be
    // unbounded.
    if (g.is_line_or_parameter()) {
      const int sp_sign = Scalar_Products::homogeneous_sign(expr, g);
      if (sp_sign != 0)
        // `*this' does not bound `expr'.
        return false;
    }
  }
  return true;
}

bool Parma_Polyhedra_Library::Grid::can_recycle_congruence_systems ( )

inlinestatic

Returns true indicating that this domain has methods that can recycle congruences.

Definition at line 297 of file Grid.inlines.hh.

                                     {
  return true;
}

bool Parma_Polyhedra_Library::Grid::can_recycle_constraint_systems ( )

inlinestatic

Returns true indicating that this domain has methods that can recycle constraints.

Definition at line 292 of file Grid.inlines.hh.

                                     {
  return true;
}

void Parma_Polyhedra_Library::Grid::clear_congruences_minimized ( )

inlineprivate

Sets status to express that congruences are no longer minimized.

Definition at line 87 of file Grid.inlines.hh.

References Parma_Polyhedra_Library::Grid::Status::reset_c_minimized(), and status.

Referenced by clear_congruences_up_to_date(), intersection_assign(), and map_space_dimensions().

                                  {
  status.reset_c_minimized();
}

void Parma_Polyhedra_Library::Grid::clear_congruences_up_to_date ( )

inlineprivate

Sets status to express that congruences are out of date.

Definition at line 97 of file Grid.inlines.hh.

References clear_congruences_minimized(), Parma_Polyhedra_Library::Grid::Status::reset_c_up_to_date(), and status.

Referenced by time_elapse_assign(), and upper_bound_assign().

                                   {
  clear_congruences_minimized();
  status.reset_c_up_to_date();
  // Can get rid of con_sys here.
}

void Parma_Polyhedra_Library::Grid::clear_empty ( )

inlineprivate

Clears the status flag indicating that the grid is empty.

Definition at line 82 of file Grid.inlines.hh.

References Parma_Polyhedra_Library::Grid::Status::reset_empty(), and status.

                  {
  status.reset_empty();
}

void Parma_Polyhedra_Library::Grid::clear_generators_minimized ( )

inlineprivate

Sets status to express that generators are no longer minimized.

Definition at line 92 of file Grid.inlines.hh.

References Parma_Polyhedra_Library::Grid::Status::reset_g_minimized(), and status.

Referenced by clear_generators_up_to_date(), map_space_dimensions(), time_elapse_assign(), and upper_bound_assign().

                                 {
  status.reset_g_minimized();
}

void Parma_Polyhedra_Library::Grid::clear_generators_up_to_date ( )

inlineprivate

Sets status to express that generators are out of date.

Definition at line 104 of file Grid.inlines.hh.

References clear_generators_minimized(), Parma_Polyhedra_Library::Grid::Status::reset_g_up_to_date(), and status.

Referenced by intersection_assign(), and OK().

                                  {
  clear_generators_minimized();
  status.reset_g_up_to_date();
  // Can get rid of gen_sys here.
}

void Parma_Polyhedra_Library::Grid::concatenate_assign ( const Grid & y )

Assigns to *this the concatenation of *this and y, taken in this order.

Exceptions:

std::length_error Thrown if the concatenation would cause the vector space to exceed dimension max_space_dimension().

Definition at line 219 of file Grid_chdims.cc.

References Parma_Polyhedra_Library::check_space_dimension_overflow(), congruences(), marked_empty(), Parma_Polyhedra_Library::max_space_dimension(), PPL_ASSERT, space_dim, and space_dimension().

                                         {
  // The space dimension of the resulting grid must be at most the
  // maximum allowed space dimension.
  check_space_dimension_overflow(y.space_dimension(),
                                 max_space_dimension() - space_dimension(),
                                 "PPL::Grid::",
                                 "concatenate_assign(y)",
                                 "concatenation exceeds the maximum "
                                 "allowed space dimension");

  const dimension_type added_columns = y.space_dim;

  // If `*this' or `y' are empty grids just adjust the space
  // dimension.
  if (marked_empty() || y.marked_empty()) {
    space_dim += added_columns;
    set_empty();
    return;
  }

  // If `y' is a universe 0-dim grid, the result is `*this'.
  if (added_columns == 0)
    return;

  // If `*this' is a universe 0-dim space grid, the result is `y'.
  if (space_dim == 0) {
    *this = y;
    return;
  }

  if (!congruences_are_up_to_date())
    update_congruences();

  con_sys.concatenate(y.congruences());

  space_dim += added_columns;

  clear_congruences_minimized();
  clear_generators_up_to_date();

  // Check that the system is OK, taking into account that the system
  // of congruences may now be empty.
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::congruence_widening_assign	(	const Grid &	y,
		unsigned *	tp = `NULL`
	)

Assigns to *this the result of computing the Grid widening between *this and y using congruence systems.

Parameters:

y	A grid that must be contained in `*this`;
tp	An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique).

Exceptions:

std::invalid_argument Thrown if *this and y are dimension-incompatible.

Definition at line 75 of file Grid_widenings.cc.

References add_recycled_congruences(), con_sys, congruences_are_minimized(), congruences_are_up_to_date(), contains(), Parma_Polyhedra_Library::copy_contains(), dim_kinds, m_swap(), marked_empty(), Parma_Polyhedra_Library::Congruence_System::num_equalities(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), OK(), PPL_ASSERT, PPL_EXPECT_HEAVY, select_wider_congruences(), set_congruences_minimized(), set_empty(), space_dim, and update_congruences().

Referenced by limited_congruence_extrapolation_assign(), and widening_assign().

                                                               {
  Grid& x = *this;
  // Dimension-compatibility check.
  if (x.space_dim != y.space_dim)
    throw_dimension_incompatible("widening_assign(y)", "y", y);

  // Assume `y' is contained in or equal to `x'.
  PPL_EXPECT_HEAVY(copy_contains(x, y));

  // Leave `x' the same if `x' or `y' is zero-dimensional or empty.
  if (x.space_dim == 0 || x.marked_empty() || y.marked_empty())
    return;

  // Ensure that the `x' congruences are in minimal form.
  if (x.congruences_are_up_to_date()) {
    if (!x.congruences_are_minimized()) {
      if (simplify(x.con_sys, x.dim_kinds)) {
        // `x' is empty.
        x.set_empty();
        return;
      }
      x.set_congruences_minimized();
    }
  }
  else
    x.update_congruences();

  // Ensure that the `y' congruences are in minimal form.
  Grid& yy = const_cast<Grid&>(y);
  if (yy.congruences_are_up_to_date()) {
    if (!yy.congruences_are_minimized()) {
      if (simplify(yy.con_sys, yy.dim_kinds)) {
        // `y' is empty.
        yy.set_empty();
        return;
      }
      yy.set_congruences_minimized();
    }
  }
  else
    yy.update_congruences();

  if (con_sys.num_equalities() < yy.con_sys.num_equalities())
    return;

  // Copy into `cgs' the congruences of `x' that are common to `y',
  // according to the grid widening.
  Congruence_System cgs;
  x.select_wider_congruences(yy, cgs);

  if (cgs.num_rows() == con_sys.num_rows())
    // All congruences were selected, thus the result is `x'.
    return;

  // A strict subset of the congruences was selected.

  Grid result(x.space_dim);
  result.add_recycled_congruences(cgs);

  // Check whether we are using the widening-with-tokens technique
  // and there are still tokens available.
  if (tp != 0 && *tp > 0) {
    // There are tokens available.  If `result' is not a subset of
    // `x', then it is less precise and we use one of the available
    // tokens.
    if (!x.contains(result))
      --(*tp);
  }
  else
    // No tokens.
    x.m_swap(result);

  PPL_ASSERT(x.OK(true));
}

const PPL::Congruence_System & Parma_Polyhedra_Library::Grid::congruences ( ) const

Returns the system of congruences.

Definition at line 281 of file Grid_public.cc.

References PPL_ASSERT.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PSET >::approximate_partition(), Parma_Polyhedra_Library::Pointset_Powerset< PSET >::approximate_partition_aux(), concatenate_assign(), constraints(), and difference_assign().

                           {
  if (marked_empty())
    return con_sys;

  if (space_dim == 0) {
    // Zero-dimensional universe.
    PPL_ASSERT(con_sys.num_rows() == 0 && con_sys.num_columns() == 2);
    return con_sys;
  }

  if (!congruences_are_up_to_date())
    update_congruences();

  return con_sys;
}

bool Parma_Polyhedra_Library::Grid::congruences_are_minimized ( ) const

inlineprivate

Returns true if the system of congruences is minimized.

Definition at line 50 of file Grid.inlines.hh.

References status, and Parma_Polyhedra_Library::Grid::Status::test_c_minimized().

Referenced by add_space_dimensions(), congruence_widening_assign(), Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate(), is_included_in(), quick_equivalence_test(), select_wider_congruences(), and simplify_using_context_assign().

                                      {
  return status.test_c_minimized();
}

bool Parma_Polyhedra_Library::Grid::congruences_are_up_to_date ( ) const

inlineprivate

Returns true if the system of congruences is up-to-date.

Definition at line 40 of file Grid.inlines.hh.

References status, and Parma_Polyhedra_Library::Grid::Status::test_c_up_to_date().

Referenced by congruence_widening_assign(), Grid(), Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate(), intersection_assign(), is_included_in(), map_space_dimensions(), operator=(), simplify_using_context_assign(), and widening_assign().

                                       {
  return status.test_c_up_to_date();
}

bool Parma_Polyhedra_Library::Grid::constrains ( Variable var ) const

Returns true if and only if var is constrained in *this.

Exceptions:

std::invalid_argument Thrown if var is not a space dimension of *this.

Definition at line 817 of file Grid_public.cc.

References Parma_Polyhedra_Library::Grid_Generator::coefficient(), Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Grid_Generator::is_line(), Parma_Polyhedra_Library::Boundary_NS::sgn(), and Parma_Polyhedra_Library::Variable::space_dimension().

                                            {
  // `var' should be one of the dimensions of the grid.
  const dimension_type var_space_dim = var.space_dimension();
  if (space_dim < var_space_dim)
    throw_dimension_incompatible("constrains(v)", "v", var);

  // An empty grid constrains all variables.
  if (marked_empty())
    return true;

  if (generators_are_up_to_date()) {
    // Since generators are up-to-date, the generator system (since it is
    // well formed) contains a point.  Hence the grid is not empty.
    if (congruences_are_up_to_date())
      // Here a variable is constrained if and only if it is
      // syntactically constrained.
      goto syntactic_check;

    if (generators_are_minimized()) {
      // Try a quick, incomplete check for the universe grid:
      // a universe grid constrains no variable.
      // Count the number of lines (they are linearly independent).
      dimension_type num_lines = 0;
      for (dimension_type i = gen_sys.num_rows(); i-- > 0; )
        if (gen_sys[i].is_line())
          ++num_lines;

      if (num_lines == space_dim)
        return false;
    }

    // Scan generators: perhaps we will find line(var).
    const dimension_type var_id = var.id();
    for (dimension_type i = gen_sys.num_rows(); i-- > 0; ) {
      const Grid_Generator& g_i = gen_sys[i];
      if (g_i.is_line()) {
        if (sgn(g_i.coefficient(var)) != 0) {
          for (dimension_type j = 0; j < space_dim; ++j)
            if (g_i.coefficient(Variable(j)) != 0 && j != var_id)
              goto next;
          return true;
        }
      }
    next:
      ;
    }

    // We are still here: at least we know that the grid is not empty.
    update_congruences();
    goto syntactic_check;
  }

  // We must minimize to detect emptiness and obtain constraints.
  if (!minimize())
    return true;

 syntactic_check:
  for (dimension_type i = con_sys.num_rows(); i-- > 0; )
    if (con_sys[i].coefficient(var) != 0)
      return true;
  return false;
}

Constraint_System Parma_Polyhedra_Library::Grid::constraints ( ) const

inline

Returns a system of equality constraints satisfied by *this with the same affine dimension as *this.

Definition at line 239 of file Grid.inlines.hh.

References congruences().

Referenced by Parma_Polyhedra_Library::C_Polyhedron::C_Polyhedron(), Parma_Polyhedra_Library::Affine_Space::constraints(), and Parma_Polyhedra_Library::NNC_Polyhedron::NNC_Polyhedron().

                        {
  return Constraint_System(congruences());
}

void Parma_Polyhedra_Library::Grid::construct	(	dimension_type	num_dimensions,
		Degenerate_Element	kind
	)

private

Builds a grid universe or empty grid.

Parameters:

num_dimensions	The number of dimensions of the vector space enclosing the grid;
kind	specifies whether the universe or the empty grid has to be built.

Definition at line 51 of file Grid_nonpublic.cc.

References con_sys, CON_VIRTUAL, dim_kinds, Parma_Polyhedra_Library::EMPTY, gen_sys, Parma_Polyhedra_Library::Congruence_System::increase_space_dimension(), Parma_Polyhedra_Library::Grid_Generator_System::insert(), Parma_Polyhedra_Library::Congruence_System::m_swap(), OK(), PPL_ASSERT, PROPER_CONGRUENCE, set_congruences_minimized(), Parma_Polyhedra_Library::Grid::Status::set_empty(), set_generators_minimized(), set_zero_dim_univ(), space_dim, status, Parma_Polyhedra_Library::Congruence::zero_dim_false(), and Parma_Polyhedra_Library::Congruence::zero_dim_integrality().

Referenced by Grid().

                                                    {
  space_dim = num_dimensions;

  if (kind == EMPTY) {
    // Set emptiness directly instead of with set_empty, as gen_sys is
    // already correctly initialized.

    status.set_empty();

    // Extend the zero dim false congruence system to the appropriate
    // dimension and then store it in `con_sys'.
    Congruence_System cgs(Congruence::zero_dim_false());
    cgs.increase_space_dimension(space_dim);
    con_sys.m_swap(cgs);

    PPL_ASSERT(OK());
    return;
  }

  if (num_dimensions > 0) {
    con_sys.increase_space_dimension(num_dimensions);

    // Initialize both systems to universe representations.

    set_congruences_minimized();
    set_generators_minimized();
    dim_kinds.resize(num_dimensions + 1);

    // Extend the zero dim integrality congruence system to the
    // appropriate dimension and then store it in `con_sys'.
    Congruence_System cgs(Congruence::zero_dim_integrality());
    cgs.increase_space_dimension(space_dim);
    cgs[0][0] = 1; // Recover minimal form after cgs(zdi) normalization.
    con_sys.m_swap(cgs);

    dim_kinds[0] = PROPER_CONGRUENCE /* a.k.a. PARAMETER */;

    // Trivially true point.
    gen_sys.insert(grid_point(0*(Variable(0))));

    // A line for each dimension.
    dimension_type dim = 0;
    while (dim < num_dimensions) {
      gen_sys.insert(grid_line(Variable(dim)));
      dim_kinds[++dim] = CON_VIRTUAL /* a.k.a. LINE */;
    }
  }
  else
    set_zero_dim_univ();
}

void Parma_Polyhedra_Library::Grid::construct ( Congruence_System & cgs )

private

Builds a grid from a system of congruences.

The grid inherits the space dimension of the congruence system.

Parameters:

cgs	The system of congruences defining the grid. Its data-structures may be recycled to build the grid.

Definition at line 104 of file Grid_nonpublic.cc.

References Parma_Polyhedra_Library::max_space_dimension(), Parma_Polyhedra_Library::Dense_Matrix::num_columns(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), PPL_ASSERT, Parma_Polyhedra_Library::Congruence_System::space_dimension(), and Parma_Polyhedra_Library::Congruence::zero_dim_false().

                                         {
  // Protecting against space dimension overflow is up to the caller.
  PPL_ASSERT(cgs.space_dimension() <= max_space_dimension());
  // Preparing con_sys and gen_sys is up to the caller.
  PPL_ASSERT(cgs.space_dimension() == con_sys.space_dimension());
  PPL_ASSERT(cgs.space_dimension() == gen_sys.space_dimension());
  PPL_ASSERT(con_sys.has_no_rows());
  PPL_ASSERT(gen_sys.has_no_rows());

  // Set the space dimension.
  space_dim = cgs.space_dimension();

  if (space_dim > 0) {
    // Stealing the rows from `cgs'.
    con_sys.m_swap(cgs);
    con_sys.normalize_moduli();
    set_congruences_up_to_date();
  }
  else {
    // Here `space_dim == 0'.
    if (cgs.num_columns() > 1)
      // See if an inconsistent congruence has been passed.
      for (dimension_type i = cgs.num_rows(); i-- > 0; )
        if (cgs[i].is_inconsistent()) {
          // Inconsistent congruence found: the grid is empty.
          status.set_empty();
          // Insert the zero dim false congruence system into `con_sys'.
          // `gen_sys' is already in empty form.
          con_sys.insert(Congruence::zero_dim_false());
          PPL_ASSERT(OK());
          return;
        }
    set_zero_dim_univ();
  }
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::construct ( Grid_Generator_System & ggs )

private

Builds a grid from a system of grid generators.

The grid inherits the space dimension of the generator system.

Parameters:

ggs	The system of grid generators defining the grid. Its data-structures may be recycled to build the grid.

Definition at line 142 of file Grid_nonpublic.cc.

References Parma_Polyhedra_Library::Dense_Matrix::has_no_rows(), Parma_Polyhedra_Library::Grid_Generator_System::has_points(), Parma_Polyhedra_Library::max_space_dimension(), PPL_ASSERT, Parma_Polyhedra_Library::Grid_Generator_System::space_dimension(), and Parma_Polyhedra_Library::Congruence::zero_dim_false().

                                             {
  // Protecting against space dimension overflow is up to the caller.
  PPL_ASSERT(ggs.space_dimension() <= max_space_dimension());
  // Preparing con_sys and gen_sys is up to the caller.
  PPL_ASSERT(ggs.space_dimension() == con_sys.space_dimension());
  PPL_ASSERT(ggs.space_dimension() == gen_sys.space_dimension());
  PPL_ASSERT(con_sys.has_no_rows());
  PPL_ASSERT(gen_sys.has_no_rows());

  // Set the space dimension.
  space_dim = ggs.space_dimension();

  // An empty set of generators defines the empty grid.
  if (ggs.has_no_rows()) {
    status.set_empty();
    // Insert the zero dim false congruence system into `con_sys'.
    // `gen_sys' is already in empty form.
    con_sys.insert(Congruence::zero_dim_false());
    return;
  }

  // Non-empty valid generator systems have a supporting point, at least.
  if (!ggs.has_points())
    throw_invalid_generators("Grid(ggs)", "ggs");

  if (space_dim == 0)
    set_zero_dim_univ();
  else {
    // Steal the rows from `ggs'.
    gen_sys.m_swap(ggs);
    normalize_divisors(gen_sys);
    // Generators are now up-to-date.
    set_generators_up_to_date();
  }

  PPL_ASSERT(OK());
}

bool Parma_Polyhedra_Library::Grid::contains ( const Grid & y ) const

Returns true if and only if *this contains y.

Exceptions:

std::invalid_argument Thrown if *this and y are dimension-incompatible.

Definition at line 2575 of file Grid_public.cc.

References is_empty(), is_included_in(), marked_empty(), quick_equivalence_test(), space_dim, and TVB_TRUE.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PSET >::check_containment(), congruence_widening_assign(), difference_assign(), generator_widening_assign(), and strictly_contains().

                                     {
  const Grid& x = *this;

  // Dimension-compatibility check.
  if (x.space_dim != y.space_dim)
    throw_dimension_incompatible("contains(y)", "y", y);

  if (y.marked_empty())
    return true;
  if (x.marked_empty())
    return y.is_empty();
  if (y.space_dim == 0)
    return true;
  if (x.quick_equivalence_test(y) == Grid::TVB_TRUE)
    return true;
  return y.is_included_in(x);
}

bool Parma_Polyhedra_Library::Grid::contains_integer_point ( ) const

Returns true if and only if *this contains at least one integer point.

Definition at line 795 of file Grid_public.cc.

References add_recycled_congruences(), Parma_Polyhedra_Library::Congruence_System::insert(), and is_empty().

                                      {
  // Empty grids have no points.
  if (marked_empty())
    return false;

  // A zero-dimensional, universe grid has, by convention, an
  // integer point.
  if (space_dim == 0)
    return true;

  // A grid has an integer point if its intersection with the integer
  // grid is non-empty.
  Congruence_System cgs;
  for (dimension_type var_index = space_dim; var_index-- > 0; )
    cgs.insert(Variable(var_index) %= 0);

  Grid gr = *this;
  gr.add_recycled_congruences(cgs);
  return !gr.is_empty();
}

void Parma_Polyhedra_Library::Grid::conversion	(	Congruence_System &	source,
		Grid_Generator_System &	dest,
		Dimension_Kinds &	dim_kinds
	)

staticprivate

Converts generator system dest to be equivalent to congruence system source.

Definition at line 312 of file Grid_conversion.cc.

References CON_VIRTUAL, dim_kinds, EQUALITY, Parma_Polyhedra_Library::exact_div_assign(), Parma_Polyhedra_Library::gcd_assign(), GEN_VIRTUAL, Parma_Polyhedra_Library::lcm_assign(), LINE, lower_triangular(), multiply_grid(), Parma_Polyhedra_Library::Dense_Matrix::num_columns(), PARAMETER, PPL_ASSERT, PPL_DIRTY_TEMP_COEFFICIENT, PROPER_CONGRUENCE, Parma_Polyhedra_Library::Grid_Generator_System::resize_no_copy(), Parma_Polyhedra_Library::Grid_Generator_System::set_index_first_pending_row(), Parma_Polyhedra_Library::Grid_Generator::set_is_line(), Parma_Polyhedra_Library::Grid_Generator::set_is_parameter_or_point(), Parma_Polyhedra_Library::sub_mul_assign(), and upper_triangular().

                                             {
  // Quite similar to the generator to congruence version above.
  // Changes here may be needed there too.

  PPL_ASSERT(lower_triangular(source, dim_kinds));

  // Initialize matrix row number counters and compute the LCM of the
  // diagonal entries of the proper congruences in `source'.
  dimension_type source_num_rows = 0, dest_num_rows = 0;
  PPL_DIRTY_TEMP_COEFFICIENT(diagonal_lcm);
  diagonal_lcm = 1;
  dimension_type dims = source.num_columns() - 1;
  for (dimension_type dim = dims; dim-- > 0; )
    if (dim_kinds[dim] == CON_VIRTUAL)
      // Virtual congruences map to lines.
      ++dest_num_rows;
    else {
      if (dim_kinds[dim] == PROPER_CONGRUENCE) {
        // Dimension `dim' has a proper congruence row at
        // `source_num_rows' in `source', so include in `diagonal_lcm'
        // the `dim'th element of that row.
        lcm_assign(diagonal_lcm, diagonal_lcm, source[source_num_rows][dim]);
        // Proper congruences map to parameters.
        ++dest_num_rows;
      }
      // Equalities map to virtual generators.
      ++source_num_rows;
    }

  // `source' must be regular.
  PPL_ASSERT(diagonal_lcm != 0);

  dest.set_index_first_pending_row(dest_num_rows);
  dest.resize_no_copy(dest_num_rows, dims + 1 /* parameter divisor */);

  // In `dest' initialize row types and elements, including setting
  // the diagonal elements to the inverse ratio of the `source'
  // diagonal elements.
  //
  // The top-down order of the congruence system rows corresponds to
  // the right-left order of the dimensions.
  dimension_type source_index = 0;
  // The generator system has a bottom-up ordering.
  dimension_type dest_index = dest_num_rows - 1;
  for (dimension_type dim = dims; dim-- > 0; ) {
    if (dim_kinds[dim] == EQUALITY) {
      ++source_index;
    }
    else {
      Grid_Generator& g = dest[dest_index];
      for (dimension_type j = dim; j-- > 0; )
        g[j] = 0;
      for (dimension_type j = dim + 1; j < dims; ++j)
        g[j] = 0;

      if (dim_kinds[dim] == CON_VIRTUAL) {
        g.set_is_line();
        g[dim] = 1;
      }
      else {
        PPL_ASSERT(dim_kinds[dim] == PROPER_CONGRUENCE);
        g.set_is_parameter_or_point();
        exact_div_assign(g[dim], diagonal_lcm, source[source_index][dim]);
        ++source_index;
      }
      --dest_index;
    }
  }

  PPL_ASSERT(upper_triangular(dest, dim_kinds));

  // Convert.
  //
  // `source_index' and `dest_index' hold the positions of pivot rows
  // in `source' and `dest'.  The order of the rows in `dest' is the
  // reverse of the order in `source', so the rows are iterated from
  // last to first (index 0) in `source' and from first to last in
  // `dest'.
  source_index = source_num_rows;
  dest_index = 0;
  PPL_DIRTY_TEMP_COEFFICIENT(reduced_source_dim);

  for (dimension_type dim = 0; dim < dims; ++dim) {
    if (dim_kinds[dim] != CON_VIRTUAL) {
      --source_index;
      const Coefficient& source_dim = source[source_index][dim];

      // In the rows in `dest' above `dest_index' divide each element
      // at column `dim' by `source_dim'.
      for (dimension_type row = dest_index; row-- > 0; ) {
        Grid_Generator& g = dest[row];

        // Multiply the representation of `dest' such that entry `dim'
        // of `g' is a multiple of `source_dim'.  This ensures that
        // the result of the division that follows is a whole number.
        gcd_assign(reduced_source_dim, g[dim], source_dim);
        exact_div_assign(reduced_source_dim, source_dim, reduced_source_dim);
        multiply_grid(reduced_source_dim, g, dest, dest_num_rows,
                      dims + 1 /* parameter divisor */);

        Coefficient& g_dim = g[dim];
        exact_div_assign(g_dim, g_dim, source_dim);
      }
    }

    // Invert and transpose the source row at `source_index' into the
    // destination row at `dest_index'.
    //
    // Consider each dimension `dim_fol' that follows `dim', as the
    // rows in `dest' that follow row `dest_index' are zero at index
    // `dim'.
    dimension_type tmp_source_index = source_index;
    if (dim_kinds[dim] != EQUALITY)
      ++dest_index;
    for (dimension_type dim_fol = dim + 1; dim_fol < dims; ++dim_fol) {
      if (dim_kinds[dim_fol] != CON_VIRTUAL) {
        --tmp_source_index;
        const Coefficient& source_dim = source[tmp_source_index][dim];
        // In order to compute the transpose of the inverse of
        // `source', subtract source[tmp_source_index][dim] times the
        // column vector in `dest' at `dim' from the column vector in
        // `dest' at `dim_fol'.
        //
        // I.e., for each row `dest_index' in `dest' that is above the
        // row `dest_index', subtract dest[tmp_source_index][dim]
        // times the entry `dim' from the entry at `dim_fol'.
        for (dimension_type row = dest_index; row-- > 0; ) {
          PPL_ASSERT(row < dest_num_rows);
          Grid_Generator& g = dest[row];
          sub_mul_assign(g[dim_fol], source_dim, g[dim]);
        }
      }
    }
  }

  PPL_ASSERT(upper_triangular(dest, dim_kinds));

  // Since we are reducing the system to "strong minimal form",
  // reduce the coordinates in the grid_generator system
  // using "diagonal" values.
  for (dimension_type dim = 0, i = 0; dim < dims; ++dim)
    if (dim_kinds[dim] != GEN_VIRTUAL)
      // Factor the "diagonal" generator out of the preceding rows.
      reduce_reduced<Grid_Generator_System, Grid_Generator>
        (dest, dim, i++, dim, dims - 1, dim_kinds);

  // Ensure that the parameter divisors are the same as the divisor of
  // the point.
  const Coefficient& system_divisor = dest[0][0];
  for (dimension_type row = dest.num_rows() - 1, dim = dims;
       dim-- > 1; )
    switch (dim_kinds[dim]) {
    case PARAMETER:
      dest[row].set_divisor(system_divisor);
      // Intentionally fall through.
    case LINE:
      --row;
      // Intentionally fall through.
    case GEN_VIRTUAL:
      break;
    }
}

void Parma_Polyhedra_Library::Grid::conversion	(	Grid_Generator_System &	source,
		Congruence_System &	dest,
		Dimension_Kinds &	dim_kinds
	)

staticprivate

Converts congruence system dest to be equivalent to generator system source.

Definition at line 154 of file Grid_conversion.cc.

References CON_VIRTUAL, dim_kinds, Parma_Polyhedra_Library::exact_div_assign(), Parma_Polyhedra_Library::gcd_assign(), GEN_VIRTUAL, Parma_Polyhedra_Library::lcm_assign(), LINE, lower_triangular(), multiply_grid(), Parma_Polyhedra_Library::Grid_Generator_System::num_rows(), PARAMETER, PPL_ASSERT, PPL_DIRTY_TEMP_COEFFICIENT, Parma_Polyhedra_Library::Congruence_System::resize_no_copy(), Parma_Polyhedra_Library::Grid_Generator_System::space_dimension(), Parma_Polyhedra_Library::sub_mul_assign(), and upper_triangular().

                                             {
  // Quite similar to the congruence to generator version below.
  // Changes here may be needed there too.

  PPL_ASSERT(upper_triangular(source, dim_kinds));

  // Initialize matrix row number counters and compute the LCM of the
  // diagonal entries of the parameters in `source'.
  //
  // The top-down order of the generator system rows corresponds to
  // the left-right order of the dimensions, while the congruence
  // system rows have a bottom-up ordering.
  dimension_type dest_num_rows = 0;
  PPL_DIRTY_TEMP_COEFFICIENT(diagonal_lcm);
  diagonal_lcm = 1;
  const dimension_type dims = source.space_dimension() + 1;
  dimension_type source_index = source.num_rows();
  for (dimension_type dim = dims; dim-- > 0; )
    if (dim_kinds[dim] == GEN_VIRTUAL)
      // Virtual generators map to equalities.
      ++dest_num_rows;
    else {
      --source_index;
      if (dim_kinds[dim] == PARAMETER) {
        // Dimension `dim' has a parameter row at `source_index' in
        // `source', so include in `diagonal_lcm' the `dim'th element
        // of that row.
        lcm_assign(diagonal_lcm, diagonal_lcm, source[source_index][dim]);
        // Parameters map to proper congruences.
        ++dest_num_rows;
      }
      // Lines map to virtual congruences.
    }
  PPL_ASSERT(source_index == 0);

  // `source' must be regular.
  PPL_ASSERT(diagonal_lcm != 0);

  dest.resize_no_copy(dest_num_rows, dims + 1 /* moduli */);

  // In `dest' initialize row types and elements, including setting
  // the diagonal elements to the inverse ratio of the `source'
  // diagonal elements.
  dimension_type dest_index = 0;
  source_index = source.num_rows();
  for (dimension_type dim = dims; dim-- > 0; ) {
    if (dim_kinds[dim] == LINE)
      --source_index;
    else {
      Congruence& cg = dest[dest_index];
      for (dimension_type j = dim; j-- > 0; )
        cg[j] = 0;
      for (dimension_type j = dim + 1; j < dims; ++j)
        cg[j] = 0;

      if (dim_kinds[dim] == GEN_VIRTUAL) {
        cg[dims] = 0;           // An equality.
        cg[dim] = 1;
      }
      else {
        PPL_ASSERT(dim_kinds[dim] == PARAMETER);
        --source_index;
        cg[dims] = 1;           // A proper congruence.
        exact_div_assign(cg[dim], diagonal_lcm, source[source_index][dim]);
      }
      ++dest_index;
    }
  }

  PPL_ASSERT(source_index == 0);
  PPL_ASSERT(dest_index == dest_num_rows);
  PPL_ASSERT(lower_triangular(dest, dim_kinds));

  // Convert.
  //
  // `source_index' and `dest_index' hold the positions of pivot rows
  // in `source' and `dest'.  The order of the rows in `dest' is the
  // reverse of the order in `source', so the rows are iterated from
  // last to first (index 0) in `source' and from first to last in
  // `dest'.
  source_index = source.num_rows();
  dest_index = 0;
  PPL_DIRTY_TEMP_COEFFICIENT(multiplier);

  for (dimension_type dim = dims; dim-- > 0; ) {
    if (dim_kinds[dim] != GEN_VIRTUAL) {
      --source_index;
      const Coefficient& source_dim = source[source_index][dim];

      // In the rows in `dest' above `dest_index' divide each element
      // at column `dim' by `source_dim'.
      for (dimension_type row = dest_index; row-- > 0; ) {
        Congruence& cg = dest[row];

        // Multiply the representation of `dest' such that entry `dim'
        // of `g' is a multiple of `source_dim'.  This ensures that
        // the result of the division that follows is a whole number.
        gcd_assign(multiplier, cg[dim], source_dim);
        exact_div_assign(multiplier, source_dim, multiplier);
        multiply_grid(multiplier, cg, dest, dest_num_rows, dims);

        Coefficient& cg_dim = cg[dim];
        exact_div_assign(cg_dim, cg_dim, source_dim);
      }
    }

    // Invert and transpose the source row at `source_index' into the
    // destination row at `dest_index'.
    //
    // Consider each dimension `dim_prec' that precedes `dim', as the
    // rows in `dest' that follow `dim_index' have zeroes at index
    // `dim'.
    dimension_type tmp_source_index = source_index;
    if (dim_kinds[dim] != LINE)
      ++dest_index;
    for (dimension_type dim_prec = dim; dim_prec-- > 0; ) {
      if (dim_kinds[dim_prec] != GEN_VIRTUAL) {
        --tmp_source_index;
        const Coefficient& source_dim = source[tmp_source_index][dim];
        // In order to compute the transpose of the inverse of
        // `source', subtract source[tmp_source_index][dim] times the
        // column vector in `dest' at `dim' from the column vector in
        // `dest' at `dim_prec'.
        //
        // I.e., for each row `dest_index' in `dest' that is above the
        // row `dest_index', subtract dest[tmp_source_index][dim]
        // times the entry `dim' from the entry at `dim_prec'.
        for (dimension_type row = dest_index; row-- > 0; ) {
          PPL_ASSERT(row < dest_num_rows);
          Congruence& cg = dest[row];
          sub_mul_assign(cg[dim_prec], source_dim, cg[dim]);
        }
      }
    }
  }
  // Set the modulus in every congruence.
  const Coefficient& modulus = dest[dest_num_rows - 1][0];
  for (dimension_type row = dest_num_rows; row-- > 0; ) {
    Congruence& cg = dest[row];
    if (cg[dims] > 0)
      // `cg' is a proper congruence.
      cg[dims] = modulus;
  }

  PPL_ASSERT(lower_triangular(dest, dim_kinds));

  // Since we are reducing the system to "strong minimal form",
  // reduce the coefficients in the congruence system
  // using "diagonal" values.
  for (dimension_type dim = dims, i = 0; dim-- > 0; )
    if (dim_kinds[dim] != CON_VIRTUAL)
      // Factor the "diagonal" congruence out of the preceding rows.
      reduce_reduced<Congruence_System, Congruence>
        (dest, dim, i++, 0, dim, dim_kinds, false);
}

void Parma_Polyhedra_Library::Grid::difference_assign ( const Grid & y )

Assigns to *this the grid-difference of *this and y.

The grid difference between grids x and y is the smallest grid containing all the points from x and y that are only in x.

Exceptions:

std::invalid_argument Thrown if *this and y are dimension-incompatible.

Definition at line 1502 of file Grid_public.cc.

References add_congruence_no_check(), Parma_Polyhedra_Library::Congruence_System::begin(), congruences(), contains(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Congruence_System::end(), Parma_Polyhedra_Library::Poly_Con_Relation::implies(), Parma_Polyhedra_Library::Poly_Con_Relation::is_included(), Parma_Polyhedra_Library::Congruence::is_proper_congruence(), marked_empty(), Parma_Polyhedra_Library::Congruence::modulus(), PPL_ASSERT, relation_with(), set_empty(), space_dim, and upper_bound_assign().

Referenced by upper_bound_assign_if_exact().

                                        {
  Grid& x = *this;
  // Dimension-compatibility check.
  if (x.space_dim != y.space_dim)
    throw_dimension_incompatible("difference_assign(y)", "y", y);

  if (y.marked_empty() || x.marked_empty())
    return;

  // If both grids are zero-dimensional, then they are necessarily
  // universe grids, so the result is empty.
  if (x.space_dim == 0) {
    x.set_empty();
    return;
  }

  if (y.contains(x)) {
    x.set_empty();
    return;
  }

  Grid new_grid(x.space_dim, EMPTY);

  const Congruence_System& y_cgs = y.congruences();
  for (Congruence_System::const_iterator i = y_cgs.begin(),
         y_cgs_end = y_cgs.end(); i != y_cgs_end; ++i) {
    const Congruence& cg = *i;

    // The 2-complement cg2 of cg = ((e %= 0) / m) is the congruence
    // defining the sets of points exactly half-way between successive
    // hyperplanes e = km and e = (k+1)m, for any integer k; that is,
    // the hyperplanes defined by 2e = (2k + 1)m, for any integer k.
    // Thus `cg2' is the congruence ((2e %= m) / 2m).

    // As the grid difference must be a grid, only add the
    // 2-complement congruence to x if the resulting grid includes all
    // the points in x that did not satisfy `cg'.

    // The 2-complement of cg can be included in the result only if x
    // holds points other than those in cg.
    if (x.relation_with(cg).implies(Poly_Con_Relation::is_included()))
      continue;

    if (cg.is_proper_congruence()) {
      const Linear_Expression e = Linear_Expression(cg);
      // Congruence cg is ((e %= 0) / m).
      const Coefficient& m = cg.modulus();
      // If x is included in the grid defined by the congruences cg
      // and its 2-complement (i.e. the grid defined by the congruence
      // (2e %= 0) / m) then add the 2-complement to the potential
      // result.
      if (x.relation_with((2*e %= 0) / m)
          .implies(Poly_Con_Relation::is_included())) {
        Grid z = x;
        z.add_congruence_no_check((2*e %= m) / (2*m));
        new_grid.upper_bound_assign(z);
        continue;
      }
    }
    return;
  }

  *this = new_grid;

  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::drop_some_non_integer_points ( Complexity_Class complexity = ANY_COMPLEXITY )

Possibly tightens *this by dropping all points with non-integer coordinates.

Parameters:

complexity This argument is ignored as the algorithm used has polynomial complexity.

Definition at line 2885 of file Grid_public.cc.

References PPL_ASSERT.

                                                      {
  if (marked_empty() || space_dim == 0)
    return;

  // By adding integral congruences for each dimension to the
  // congruence system, defining \p *this, the grid will keep only
  // those points that have integral coordinates. All points in \p
  // *this with non-integral coordinates are removed.
  for (dimension_type i = space_dim; i-- > 0; )
    add_congruence(Variable(i) %= 0);

  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::drop_some_non_integer_points	(	const Variables_Set &	vars,
		Complexity_Class	complexity = `ANY_COMPLEXITY`
	)

Possibly tightens *this by dropping all points with non-integer coordinates for the space dimensions corresponding to vars.

Parameters:

vars	Points with non-integer coordinates for these variables/space-dimensions can be discarded.
complexity	This argument is ignored as the algorithm used has polynomial complexity.

Definition at line 2900 of file Grid_public.cc.

References PPL_ASSERT, and Parma_Polyhedra_Library::Variables_Set::space_dimension().

                                                          {
  // Dimension-compatibility check.
  const dimension_type min_space_dim = vars.space_dimension();
  if (space_dimension() < min_space_dim)
    throw_dimension_incompatible("drop_some_non_integer_points(vs, cmpl)",
                                 min_space_dim);

  if (marked_empty() || min_space_dim == 0)
    return;

  // By adding the integral congruences for each dimension in vars to
  // the congruence system defining \p *this, the grid will keep only
  // those points that have integer coordinates for all the dimensions
  // in vars. All points in \p *this with non-integral coordinates for
  // the dimensions in vars are removed.
  for (Variables_Set::const_iterator i = vars.begin(),
         vars_end = vars.end(); i != vars_end; ++i)
    add_congruence(Variable(*i) %= 0);

  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::expand_space_dimension	(	Variable	var,
		dimension_type	m
	)

Creates m copies of the space dimension corresponding to var.

Parameters:

var	The variable corresponding to the space dimension to be replicated;
m	The number of replicas to be created.

Exceptions:

std::invalid_argument	Thrown if `var` does not correspond to a dimension of the vector space.
std::length_error	Thrown if adding `m` new space dimensions would cause the vector space to exceed dimension `max_space_dimension()`.

If *this has space dimension $n$ , with $n > 0$ , and var has space dimension $k \leq n$ , then the $k$ -th space dimension is expanded to m new space dimensions $n$ , $n+1$ , $\dots$ , $n+m-1$ .

Definition at line 401 of file Grid_chdims.cc.

                                                              {
  // TODO: this implementation is _really_ an executable specification.

  // `var' must be one of the dimensions of the vector space.
  if (var.space_dimension() > space_dim)
    throw_dimension_incompatible("expand_space_dimension(v, m)", "v", var);

  // Adding 0 dimensions leaves the same grid.
  if (m == 0)
    return;

  // The resulting space dimension must be at most the maximum.
  check_space_dimension_overflow(m, max_space_dimension() - space_dimension(),
                                 "PPL::Grid::",
                                 "expand_space_dimension(v, m)",
                                 "adding m new space dimensions exceeds "
                                 "the maximum allowed space dimension");

  // Save the number of dimensions before adding new ones.
  dimension_type old_dim = space_dim;

  // Add the required new dimensions.
  add_space_dimensions_and_embed(m);

  const dimension_type src_d = var.id();
  const Congruence_System& cgs = congruences();
  Congruence_System new_congruences;
  for (Congruence_System::const_iterator i = cgs.begin(),
         cgs_end = cgs.end(); i != cgs_end; ++i) {
    const Congruence& cg = *i;

    // Only consider congruences that constrain `var'.
    if (cg.coefficient(var) == 0)
      continue;

    // Each relevant congruence results in `m' new congruences.
    for (dimension_type dst_d = old_dim; dst_d < old_dim+m; ++dst_d) {
      Linear_Expression e;
      for (dimension_type j = old_dim; j-- > 0; )
        e +=
          cg.coefficient(Variable(j))
          * ((j == src_d) ? Variable(dst_d) : Variable(j));
      new_congruences.insert_verbatim((e + cg.inhomogeneous_term() %= 0)
                                      / cg.modulus());
    }
  }
  add_recycled_congruences(new_congruences);
  PPL_ASSERT(OK());
}

PPL::memory_size_type Parma_Polyhedra_Library::Grid::external_memory_in_bytes ( ) const

Returns the size in bytes of the memory managed by *this.

Definition at line 2698 of file Grid_public.cc.

Referenced by total_memory_in_bytes().

                                        {
  return
    con_sys.external_memory_in_bytes()
    + gen_sys.external_memory_in_bytes();
}

void Parma_Polyhedra_Library::Grid::fold_space_dimensions	(	const Variables_Set &	vars,
		Variable	dest
	)

Folds the space dimensions in vars into dest.

Parameters:

vars	The set of Variable objects corresponding to the space dimensions to be folded;
dest	The variable corresponding to the space dimension that is the destination of the folding operation.

Exceptions:

std::invalid_argument Thrown if *this is dimension-incompatible with dest or with one of the Variable objects contained in vars. Also thrown if dest is contained in vars.

If *this has space dimension $n$ , with $n > 0$ , dest has space dimension $k \leq n$ , vars is a set of variables whose maximum space dimension is also less than or equal to $n$ , and dest is not a member of vars, then the space dimensions corresponding to variables in vars are folded into the $k$ -th space dimension.

Definition at line 452 of file Grid_chdims.cc.

References affine_image(), Parma_Polyhedra_Library::Variable::id(), PPL_ASSERT, Parma_Polyhedra_Library::Variables_Set::space_dimension(), Parma_Polyhedra_Library::Variable::space_dimension(), and Parma_Polyhedra_Library::upper_bound_assign().

                                                                       {
  // TODO: this implementation is _really_ an executable specification.

  // `dest' should be one of the dimensions of the grid.
  if (dest.space_dimension() > space_dim)
    throw_dimension_incompatible("fold_space_dimensions(vs, v)", "v", dest);

  // Folding only has effect if dimensions are given.
  if (vars.empty())
    return;

  // All variables in `vars' must be dimensions of the grid.
  if (vars.space_dimension() > space_dim)
    throw_dimension_incompatible("fold_space_dimensions(vs, v)",
                                 "vs.space_dimension()",
                                 vars.space_dimension());

  // Moreover, `dest.id()' must not occur in `vars'.
  if (vars.find(dest.id()) != vars.end())
    throw_invalid_argument("fold_space_dimensions(vs, v)",
                           "v should not occur in vs");
  // All of the affine images we are going to compute are not invertible,
  // hence we will need to compute the grid generators of the polyhedron.
  // Since we keep taking copies, make sure that a single conversion
  // from congruences to grid generators is computed.
  (void) grid_generators();
  // Having grid generators, we now know if the grid is empty:
  // in that case, folding is equivalent to just removing space dimensions.
  if (!marked_empty()) {
    for (Variables_Set::const_iterator i = vars.begin(),
           vs_end = vars.end(); i != vs_end; ++i) {
      Grid copy = *this;
      copy.affine_image(dest, Linear_Expression(Variable(*i)));
      upper_bound_assign(copy);
    }
  }
  remove_space_dimensions(vars);
  PPL_ASSERT(OK());
}

bool Parma_Polyhedra_Library::Grid::frequency	(	const Linear_Expression &	expr,
		Coefficient &	freq_n,
		Coefficient &	freq_d,
		Coefficient &	val_n,
		Coefficient &	val_d
	)		const

Returns true if and only if *this is not empty and frequency for *this with respect to expr is defined, in which case the frequency and the value for expr that is closest to zero are computed.

Parameters:

expr	The linear expression for which the frequency is needed;
freq_n	The numerator of the maximum frequency of `expr`;
freq_d	The denominator of the maximum frequency of `expr`;
val_n	The numerator of them value of `expr` at a point in the grid that is closest to zero;
val_d	The denominator of a value of `expr` at a point in the grid that is closest to zero;

Exceptions:

std::invalid_argument Thrown if expr and *this are dimension-incompatible.

If *this is empty or frequency is undefined with respect to expr, then false is returned and freq_n, freq_d, val_n and val_d are left untouched.

Definition at line 2519 of file Grid_public.cc.

References Parma_Polyhedra_Library::Linear_Expression::space_dimension().

Referenced by Parma_Polyhedra_Library::Affine_Space::frequency().

                                                                   {
  // The dimension of `expr' must be at most the dimension of *this.
  if (space_dim < expr.space_dimension())
    throw_dimension_incompatible("frequency(e, ...)", "e", expr);

  // Space dimension is 0: if empty, then return false;
  // otherwise the frequency is 1 and the value is 0.
  if (space_dim == 0) {
    if (is_empty())
      return false;
    freq_n = 0;
    freq_d = 1;
    val_n = 0;
    val_d = 1;
    return true;
  }
  if (!generators_are_minimized() && !minimize())
    // Minimizing found `this' empty.
    return false;

  return frequency_no_check(expr, freq_n, freq_d, val_n, val_d);
}

bool Parma_Polyhedra_Library::Grid::frequency_no_check	(	const Linear_Expression &	expr,
		Coefficient &	freq_n,
		Coefficient &	freq_d,
		Coefficient &	val_n,
		Coefficient &	val_d
	)		const

private

Returns true if and only if *this is not empty and frequency for *this with respect to expr is defined, in which case the frequency and the value for expr that is closest to zero are computed.

Parameters:

expr	The linear expression for which the frequency is needed;
freq_n	The numerator of the maximum frequency of `expr`;
freq_d	The denominator of the maximum frequency of `expr`;
val_n	The numerator of a value of `expr` at a point in the grid that is closest to zero;
val_d	The denominator of a value of `expr` at a point in the grid that is closest to zero;

If *this is empty or frequency is undefined with respect to expr, then false is returned and freq_n, freq_d, val_n and val_d are left untouched.

Warning:: If expr and *this are dimension-incompatible, the grid generator system is not minimized or *this is empty, then the behavior is undefined.

Definition at line 314 of file Grid_nonpublic.cc.

Referenced by wrap_assign().

                                                                   {

  // The dimension of `expr' must be at most the dimension of *this.
  PPL_ASSERT(space_dim >= expr.space_dimension());
  PPL_ASSERT(generators_are_minimized() && !marked_empty());

  // The generators are up to date and minimized and the grid is non-empty.

  // If the grid is bounded for the expression `expr',
  // then `expr' has a constant value and the frequency is 0.
  if (bounds_no_check(expr)) {
    freq_n = 0;
    freq_d = 1;
    // Find the value of the constant expression.
    const Grid_Generator& point = gen_sys[0];
    val_d = point.divisor();
    Scalar_Products::homogeneous_assign(val_n, expr, point);
    val_n += expr.inhomogeneous_term() * val_d;
    // Reduce `val_n' and `val_d'.
    PPL_DIRTY_TEMP_COEFFICIENT(gcd);
    gcd_assign(gcd, val_n, val_d);
    exact_div_assign(val_n, val_n, gcd);
    exact_div_assign(val_d, val_d, gcd);
    return true;
  }

  // The frequency is the gcd of the scalar products of the parameters
  // in `gen_sys'.
  dimension_type num_rows = gen_sys.num_rows();
  PPL_DIRTY_TEMP_COEFFICIENT(sp);
  freq_n = 0;

  // As the generators are minimized, `gen_sys[0]' is a point
  // and considered later.
  for (dimension_type row = 1; row < num_rows; ++row) {
    const Grid_Generator& gen = gen_sys[row];
    Scalar_Products::homogeneous_assign(sp, expr, gen);
    if (gen.is_line()) {
      if (sgn(sp) != 0)
          return false;
      continue;
    }
    // `gen' must be a parameter.
    PPL_ASSERT(gen.is_parameter());
    if (sgn(sp) != 0)
    gcd_assign(freq_n, freq_n, sp);
  }
  const Grid_Generator& point = gen_sys[0];
  PPL_ASSERT(point.is_point());

  // The denominator of the frequency and of the value is
  // the divisor for the generators.
  freq_d = point.divisor();
  val_d = freq_d;

  // As point is a grid generator, homogeneous_assign() must be used.
  Scalar_Products::homogeneous_assign(val_n, expr, point);
  val_n += expr.inhomogeneous_term() * val_d;

  // Reduce `val_n' by the frequency `freq_n'.
  val_n %= freq_n;

  PPL_DIRTY_TEMP_COEFFICIENT(gcd);
  // Reduce `freq_n' and `freq_d'.
  gcd_assign(gcd, freq_n, freq_d);
  exact_div_assign(freq_n, freq_n, gcd);
  exact_div_assign(freq_d, freq_d, gcd);

  // Reduce `val_n' and `val_d'.
  gcd_assign(gcd, val_n, val_d);
  exact_div_assign(val_n, val_n, gcd);
  exact_div_assign(val_d, val_d, gcd);

  return true;
}

void Parma_Polyhedra_Library::Grid::generalized_affine_image	(	Variable	var,
		Relation_Symbol	relsym,
		const Linear_Expression &	expr,
		Coefficient_traits::const_reference	denominator = `Coefficient_one()`,
		Coefficient_traits::const_reference	modulus = `Coefficient_zero()`
	)

Assigns to *this the image of *this with respect to the generalized affine relation $\mathrm{var}' = \frac{\mathrm{expr}}{\mathrm{denominator}} \pmod{\mathrm{modulus}}$ .

Parameters:

var	The left hand side variable of the generalized affine relation;
relsym	The relation symbol where EQUAL is the symbol for a congruence relation;
expr	The numerator of the right hand side affine expression;
denominator	The denominator of the right hand side affine expression. Optional argument with an automatic value of one;
modulus	The modulus of the congruence lhs %= rhs. A modulus of zero indicates lhs == rhs. Optional argument with an automatic value of zero.

Exceptions:

std::invalid_argument Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a space dimension of *this.

Definition at line 1930 of file Grid_public.cc.

References Parma_Polyhedra_Library::EQUAL, Parma_Polyhedra_Library::NOT_EQUAL, PPL_ASSERT, Parma_Polyhedra_Library::Variable::space_dimension(), and Parma_Polyhedra_Library::Linear_Expression::space_dimension().

                                                                    {
  // The denominator cannot be zero.
  if (denominator == 0)
    throw_invalid_argument("generalized_affine_image(v, r, e, d, m)",
                           "d == 0");

  // Dimension-compatibility checks.
  // The dimension of `expr' should not be greater than the dimension
  // of `*this'.
  const dimension_type expr_space_dim = expr.space_dimension();
  if (space_dim < expr_space_dim)
    throw_dimension_incompatible("generalized_affine_image(v, r, e, d, m)",
                                 "e", expr);
  // `var' should be one of the dimensions of the grid.
  const dimension_type var_space_dim = var.space_dimension();
  if (space_dim < var_space_dim)
    throw_dimension_incompatible("generalized_affine_image(v, r, e, d, m)",
                                 "v", var);
  // The relation symbol cannot be a disequality.
  if (relsym == NOT_EQUAL)
    throw_invalid_argument("generalized_affine_image(v, r, e, d, m)",
                           "r is the disequality relation symbol");

  // Any image of an empty grid is empty.
  if (marked_empty())
    return;

  // If relsym is not EQUAL, then we return a safe approximation
  // by adding a line in the direction of var.
  if (relsym != EQUAL) {

    if (modulus != 0)
      throw_invalid_argument("generalized_affine_image(v, r, e, d, m)",
                             "r != EQUAL && m != 0");

    if (!generators_are_up_to_date())
      minimize();

    // Any image of an empty grid is empty.
    if (marked_empty())
      return;

    add_grid_generator(grid_line(var));

    PPL_ASSERT(OK());
    return;
  }

  PPL_ASSERT(relsym == EQUAL);

  affine_image(var, expr, denominator);

  if (modulus == 0)
    return;

  // Modulate dimension `var' according to `modulus'.

  if (!generators_are_up_to_date())
    minimize();

  // Test if minimization, possibly in affine_image, found an empty
  // grid.
  if (marked_empty())
    return;

  if (modulus < 0)
    gen_sys.insert(parameter(-modulus * var));
  else
    gen_sys.insert(parameter(modulus * var));

  normalize_divisors(gen_sys);

  clear_generators_minimized();
  clear_congruences_up_to_date();

  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::generalized_affine_image	(	const Linear_Expression &	lhs,
		Relation_Symbol	relsym,
		const Linear_Expression &	rhs,
		Coefficient_traits::const_reference	modulus = `Coefficient_zero()`
	)

Assigns to *this the image of *this with respect to the generalized affine relation $\mathrm{lhs}' = \mathrm{rhs} \pmod{\mathrm{modulus}}$ .

Parameters:

lhs	The left hand side affine expression.
relsym	The relation symbol where EQUAL is the symbol for a congruence relation;
rhs	The right hand side affine expression.
modulus	The modulus of the congruence lhs %= rhs. A modulus of zero indicates lhs == rhs. Optional argument with an automatic value of zero.

Exceptions:

std::invalid_argument Thrown if *this is dimension-incompatible with lhs or rhs.

Definition at line 2111 of file Grid_public.cc.

References Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::EQUAL, Parma_Polyhedra_Library::Grid_Generator_System::insert(), Parma_Polyhedra_Library::neg_assign(), Parma_Polyhedra_Library::NOT_EQUAL, PPL_ASSERT, PPL_DIRTY_TEMP_COEFFICIENT, and Parma_Polyhedra_Library::Linear_Expression::space_dimension().

                                                                    {
  // Dimension-compatibility checks.
  // The dimension of `lhs' should be at most the dimension of
  // `*this'.
  dimension_type lhs_space_dim = lhs.space_dimension();
  if (space_dim < lhs_space_dim)
    throw_dimension_incompatible("generalized_affine_image(e1, r, e2, m)",
                                 "e1", lhs);
  // The dimension of `rhs' should be at most the dimension of
  // `*this'.
  const dimension_type rhs_space_dim = rhs.space_dimension();
  if (space_dim < rhs_space_dim)
    throw_dimension_incompatible("generalized_affine_image(e1, r, e2, m)",
                                 "e2", rhs);
  // The relation symbol cannot be a disequality.
  if (relsym == NOT_EQUAL)
    throw_invalid_argument("generalized_affine_image(e1, r, e2, m)",
                           "r is the disequality relation symbol");

  // Any image of an empty grid is empty.
  if (marked_empty())
    return;

  // If relsym is not EQUAL, then we return a safe approximation
  // by adding a line in the direction of var.
  if (relsym != EQUAL) {

    if (modulus != 0)
      throw_invalid_argument("generalized_affine_image(e1, r, e2, m)",
                             "r != EQUAL && m != 0");

    if (!generators_are_up_to_date())
      minimize();

    // Any image of an empty grid is empty.
    if (marked_empty())
      return;

    for (dimension_type i = space_dim; i-- > 0; )
      if (lhs.coefficient(Variable(i)) != 0)
        add_grid_generator(grid_line(Variable(i)));

    PPL_ASSERT(OK());
    return;
  }

  PPL_ASSERT(relsym == EQUAL);

  PPL_DIRTY_TEMP_COEFFICIENT(tmp_modulus);
  tmp_modulus = modulus;
  if (tmp_modulus < 0)
    neg_assign(tmp_modulus);

  // Compute the actual space dimension of `lhs',
  // i.e., the highest dimension having a non-zero coefficient in `lhs'.
  do {
    if (lhs_space_dim == 0) {
      // All variables have zero coefficients, so `lhs' is a constant.
      add_congruence_no_check((lhs %= rhs) / tmp_modulus);
      return;
    }
  }
  while (lhs.coefficient(Variable(--lhs_space_dim)) == 0);

  // Gather in `new_lines' the collections of all the lines having the
  // direction of variables occurring in `lhs'.  While at it, check
  // whether there exists a variable occurring in both `lhs' and
  // `rhs'.
  Grid_Generator_System new_lines;
  bool lhs_vars_intersect_rhs_vars = false;
  for (dimension_type i = lhs_space_dim + 1; i-- > 0; )
    if (lhs.coefficient(Variable(i)) != 0) {
      new_lines.insert(grid_line(Variable(i)));
      if (rhs.coefficient(Variable(i)) != 0)
        lhs_vars_intersect_rhs_vars = true;
    }

  if (lhs_vars_intersect_rhs_vars) {
    // Some variables in `lhs' also occur in `rhs'.
    // To ease the computation, add an additional dimension.
    const Variable new_var(space_dim);
    add_space_dimensions_and_embed(1);

    // Constrain the new dimension to be equal to the right hand side.
    // TODO: Use add_congruence() when it has been updated.
    Congruence_System new_cgs1(new_var == rhs);
    add_recycled_congruences(new_cgs1);
    if (!is_empty()) {
      // The grid still contains points.

      // Existentially quantify all the variables occurring in the left
      // hand side expression.

      // Adjust `new_lines' to the right dimension.
      new_lines.insert(parameter(0*Variable(space_dim-1)));
      // Add the lines to `gen_sys' (first make sure they are up-to-date).
      update_generators();
      gen_sys.recycling_insert(new_lines);
      normalize_divisors(gen_sys);
      // Update the flags.
      clear_congruences_up_to_date();
      clear_generators_minimized();

      // Constrain the new dimension so that it is congruent to the left
      // hand side expression modulo `modulus'.
      // TODO: Use add_congruence() when it has been updated.
      Congruence_System new_cgs2((lhs %= new_var) / tmp_modulus);
      add_recycled_congruences(new_cgs2);
    }

    // Remove the temporarily added dimension.
    remove_higher_space_dimensions(space_dim-1);
  }
  else {
    // `lhs' and `rhs' variables are disjoint:
    // there is no need to add a further dimension.

    // Only add the lines and congruence if there are points.
    if (is_empty())
      return;

    // Existentially quantify all the variables occurring in the left hand
    // side expression.
    add_recycled_grid_generators(new_lines);

    // Constrain the left hand side expression so that it is congruent to
    // the right hand side expression modulo `modulus'.
    add_congruence_no_check((lhs %= rhs) / tmp_modulus);
  }

  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::generalized_affine_preimage	(	Variable	var,
		Relation_Symbol	relsym,
		const Linear_Expression &	expr,
		Coefficient_traits::const_reference	denominator = `Coefficient_one()`,
		Coefficient_traits::const_reference	modulus = `Coefficient_zero()`
	)

Assigns to *this the preimage of *this with respect to the generalized affine relation $\mathrm{var}' = \frac{\mathrm{expr}}{\mathrm{denominator}} \pmod{\mathrm{modulus}}$ .

Parameters:

var	The left hand side variable of the generalized affine relation;
relsym	The relation symbol where EQUAL is the symbol for a congruence relation;
expr	The numerator of the right hand side affine expression;
denominator	The denominator of the right hand side affine expression. Optional argument with an automatic value of one;
modulus	The modulus of the congruence lhs %= rhs. A modulus of zero indicates lhs == rhs. Optional argument with an automatic value of zero.

Exceptions:

std::invalid_argument Thrown if denominator is zero or if expr and *this are dimension-incompatible or if var is not a space dimension of *this.

Definition at line 2014 of file Grid_public.cc.

References Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::EQUAL, Parma_Polyhedra_Library::neg_assign(), Parma_Polyhedra_Library::NOT_EQUAL, PPL_ASSERT, PPL_DIRTY_TEMP_COEFFICIENT, Parma_Polyhedra_Library::Variable::space_dimension(), and Parma_Polyhedra_Library::Linear_Expression::space_dimension().

                                                                       {
  // The denominator cannot be zero.
  if (denominator == 0)
    throw_invalid_argument("generalized_affine_preimage(v, r, e, d, m)",
                           "d == 0");

  // The dimension of `expr' should be at most the dimension of
  // `*this'.
  const dimension_type expr_space_dim = expr.space_dimension();
  if (space_dim < expr_space_dim)
    throw_dimension_incompatible("generalized_affine_preimage(v, r, e, d, m)",
                                 "e", expr);
  // `var' should be one of the dimensions of the grid.
  const dimension_type var_space_dim = var.space_dimension();
  if (space_dim < var_space_dim)
    throw_dimension_incompatible("generalized_affine_preimage(v, r, e, d, m)",
                                 "v", var);
  // The relation symbol cannot be a disequality.
  if (relsym == NOT_EQUAL)
    throw_invalid_argument("generalized_affine_preimage(v, r, e, d, m)",
                           "r is the disequality relation symbol");

  // If relsym is not EQUAL, then we return a safe approximation
  // by adding a line in the direction of var.
  if (relsym != EQUAL) {

    if (modulus != 0)
      throw_invalid_argument("generalized_affine_preimage(v, r, e, d, m)",
                             "r != EQUAL && m != 0");

    if (!generators_are_up_to_date())
      minimize();

    // Any image of an empty grid is empty.
    if (marked_empty())
      return;

    add_grid_generator(grid_line(var));

    PPL_ASSERT(OK());
    return;
  }

  PPL_ASSERT(relsym == EQUAL);
  // Any image of an empty grid is empty.
  if (marked_empty())
    return;

  // Check whether the affine relation is an affine function.
  if (modulus == 0) {
    affine_preimage(var, expr, denominator);
    return;
  }

  // Check whether the preimage of this affine relation can be easily
  // computed as the image of its inverse relation.
  const Coefficient& var_coefficient = expr.coefficient(var);
  if (var_space_dim <= expr_space_dim && var_coefficient != 0) {
    Linear_Expression inverse_expr
      = expr - (denominator + var_coefficient) * var;
    PPL_DIRTY_TEMP_COEFFICIENT(inverse_denominator);
    neg_assign(inverse_denominator, var_coefficient);
    if (modulus < 0)
      generalized_affine_image(var, EQUAL, inverse_expr, inverse_denominator,
                               - modulus);
    else
      generalized_affine_image(var, EQUAL, inverse_expr, inverse_denominator,
                               modulus);
    return;
  }

  // Here `var_coefficient == 0', so that the preimage cannot be
  // easily computed by inverting the affine relation.  Add the
  // congruence induced by the affine relation.
  {
    Congruence cg((denominator*var %= expr) / denominator);
    if (modulus < 0)
      cg /= -modulus;
    else
      cg /= modulus;
    add_congruence_no_check(cg);
  }

  // If the resulting grid is empty, its preimage is empty too.
  // Note: DO check for emptiness here, as we will later add a line.
  if (is_empty())
    return;
  add_grid_generator(grid_line(var));
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::generalized_affine_preimage	(	const Linear_Expression &	lhs,
		Relation_Symbol	relsym,
		const Linear_Expression &	rhs,
		Coefficient_traits::const_reference	modulus = `Coefficient_zero()`
	)

Assigns to *this the preimage of *this with respect to the generalized affine relation $\mathrm{lhs}' = \mathrm{rhs} \pmod{\mathrm{modulus}}$ .

Parameters:

lhs	The left hand side affine expression;
relsym	The relation symbol where EQUAL is the symbol for a congruence relation;
rhs	The right hand side affine expression;
modulus	The modulus of the congruence lhs %= rhs. A modulus of zero indicates lhs == rhs. Optional argument with an automatic value of zero.

Exceptions:

std::invalid_argument Thrown if *this is dimension-incompatible with lhs or rhs.

Definition at line 2249 of file Grid_public.cc.

References Parma_Polyhedra_Library::Linear_Expression::coefficient(), Parma_Polyhedra_Library::EQUAL, Parma_Polyhedra_Library::Grid_Generator_System::insert(), Parma_Polyhedra_Library::neg_assign(), Parma_Polyhedra_Library::NOT_EQUAL, PPL_ASSERT, PPL_DIRTY_TEMP_COEFFICIENT, and Parma_Polyhedra_Library::Linear_Expression::space_dimension().

                                                                       {
  // The dimension of `lhs' must be at most the dimension of `*this'.
  dimension_type lhs_space_dim = lhs.space_dimension();
  if (space_dim < lhs_space_dim)
    throw_dimension_incompatible("generalized_affine_preimage(e1, r, e2, m)",
                                 "lhs", lhs);
  // The dimension of `rhs' must be at most the dimension of `*this'.
  const dimension_type rhs_space_dim = rhs.space_dimension();
  if (space_dim < rhs_space_dim)
    throw_dimension_incompatible("generalized_affine_preimage(e1, r, e2, m)",
                                 "e2", rhs);
  // The relation symbol cannot be a disequality.
  if (relsym == NOT_EQUAL)
    throw_invalid_argument("generalized_affine_preimage(e1, r, e2, m)",
                           "r is the disequality relation symbol");

  // Any preimage of an empty grid is empty.
  if (marked_empty())
    return;

  // If relsym is not EQUAL, then we return a safe approximation
  // by adding a line in the direction of var.
  if (relsym != EQUAL) {

    if (modulus != 0)
      throw_invalid_argument("generalized_affine_preimage(e1, r, e2, m)",
                             "r != EQUAL && m != 0");

    if (!generators_are_up_to_date())
      minimize();

    // Any image of an empty grid is empty.
    if (marked_empty())
      return;

    for (dimension_type i = lhs_space_dim + 1; i-- > 0; )
      if (lhs.coefficient(Variable(i)) != 0)
        add_grid_generator(grid_line(Variable(i)));

    PPL_ASSERT(OK());
    return;
  }

  PPL_ASSERT(relsym == EQUAL);

  PPL_DIRTY_TEMP_COEFFICIENT(tmp_modulus);
  tmp_modulus = modulus;
  if (tmp_modulus < 0)
    neg_assign(tmp_modulus);

  // Compute the actual space dimension of `lhs',
  // i.e., the highest dimension having a non-zero coefficient in `lhs'.
  do {
    if (lhs_space_dim == 0) {
      // All variables have zero coefficients, so `lhs' is a constant.
      // In this case, preimage and image happen to be the same.
      add_congruence_no_check((lhs %= rhs) / tmp_modulus);
      return;
    }
  }
  while (lhs.coefficient(Variable(--lhs_space_dim)) == 0);

  // Gather in `new_lines' the collections of all the lines having
  // the direction of variables occurring in `lhs'.
  // While at it, check whether or not there exists a variable
  // occurring in both `lhs' and `rhs'.
  Grid_Generator_System new_lines;
  bool lhs_vars_intersect_rhs_vars = false;
  for (dimension_type i = lhs_space_dim + 1; i-- > 0; )
    if (lhs.coefficient(Variable(i)) != 0) {
      new_lines.insert(grid_line(Variable(i)));
      if (rhs.coefficient(Variable(i)) != 0)
        lhs_vars_intersect_rhs_vars = true;
    }

  if (lhs_vars_intersect_rhs_vars) {
    // Some variables in `lhs' also occur in `rhs'.
    // To ease the computation, add an additional dimension.
    const Variable new_var(space_dim);
    add_space_dimensions_and_embed(1);

    // Constrain the new dimension to be equal to `lhs'
    // TODO: Use add_congruence() when it has been updated.
    Congruence_System new_cgs1(new_var == lhs);
    add_recycled_congruences(new_cgs1);
    if (!is_empty()) {
      // The grid still contains points.

      // Existentially quantify all the variables occurring in the left
      // hand side

      // Adjust `new_lines' to the right dimension.
      new_lines.insert(parameter(0*Variable(space_dim-1)));
      // Add the lines to `gen_sys' (first make sure they are up-to-date).
      update_generators();
      gen_sys.recycling_insert(new_lines);
      normalize_divisors(gen_sys);
      // Update the flags.
      clear_congruences_up_to_date();
      clear_generators_minimized();

      // Constrain the new dimension so that it is related to
      // the right hand side modulo `modulus'.
      // TODO: Use add_congruence() when it has been updated.
      Congruence_System new_cgs2((rhs %= new_var) / tmp_modulus);
      add_recycled_congruences(new_cgs2);
    }

    // Remove the temporarily added dimension.
    remove_higher_space_dimensions(space_dim-1);
  }
  else {
    // `lhs' and `rhs' variables are disjoint:
    // there is no need to add a further dimension.

    // Constrain the left hand side expression so that it is congruent to
    // the right hand side expression modulo `mod'.
    add_congruence_no_check((lhs %= rhs) / tmp_modulus);

    // Any image of an empty grid is empty.
    if (is_empty())
      return;

    // Existentially quantify all the variables occurring in `lhs'.
    add_recycled_grid_generators(new_lines);
  }
  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::generator_widening_assign	(	const Grid &	y,
		unsigned *	tp = `NULL`
	)

Assigns to *this the result of computing the Grid widening between *this and y using generator systems.

Parameters:

y	A grid that must be contained in `*this`;
tp	An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique).

Exceptions:

std::invalid_argument Thrown if *this and y are dimension-incompatible.

Definition at line 264 of file Grid_widenings.cc.

References add_recycled_grid_generators(), contains(), Parma_Polyhedra_Library::copy_contains(), dim_kinds, Parma_Polyhedra_Library::EMPTY, gen_sys, generators_are_minimized(), generators_are_up_to_date(), Parma_Polyhedra_Library::Dense_Matrix::has_no_rows(), m_swap(), marked_empty(), Parma_Polyhedra_Library::Grid_Generator_System::num_lines(), Parma_Polyhedra_Library::Grid_Generator_System::num_parameters(), Parma_Polyhedra_Library::Grid_Generator_System::num_rows(), OK(), PPL_ASSERT, PPL_EXPECT_HEAVY, select_wider_generators(), set_generators_minimized(), space_dim, and update_generators().

Referenced by limited_generator_extrapolation_assign(), and widening_assign().

                                                              {
  Grid& x = *this;

  // Dimension-compatibility check.
  if (x.space_dim != y.space_dim)
    throw_dimension_incompatible("generator_widening_assign(y)", "y", y);

  // Assume `y' is contained in or equal to `x'.
  PPL_EXPECT_HEAVY(copy_contains(x, y));

  // Leave `x' the same if `x' or `y' is zero-dimensional or empty.
  if (x.space_dim == 0 || x.marked_empty() || y.marked_empty())
    return;

  // Ensure that the `x' generators are in minimal form.
  if (x.generators_are_up_to_date()) {
    if (!x.generators_are_minimized()) {
      simplify(x.gen_sys, x.dim_kinds);
      PPL_ASSERT(!x.gen_sys.has_no_rows());
      x.set_generators_minimized();
    }
  }
  else
    x.update_generators();

  if (x.marked_empty())
    return;

  // Ensure that the `y' generators are in minimal form.
  Grid& yy = const_cast<Grid&>(y);
  if (yy.generators_are_up_to_date()) {
    if (!yy.generators_are_minimized()) {
      simplify(yy.gen_sys, yy.dim_kinds);
      PPL_ASSERT(!yy.gen_sys.has_no_rows());
      yy.set_generators_minimized();
    }
  }
  else
    yy.update_generators();

  if (gen_sys.num_rows() > yy.gen_sys.num_rows())
    return;

  if (gen_sys.num_lines() > yy.gen_sys.num_lines())
    return;

  // Copy into `ggs' the generators of `x' that are common to `y',
  // according to the grid widening.
  Grid_Generator_System ggs;
  x.select_wider_generators(yy, ggs);

  if (ggs.num_parameters() == gen_sys.num_parameters())
    // All parameters are kept as parameters, thus the result is `x'.
    return;

  // A strict subset of the parameters was selected.

  Grid result(x.space_dim, EMPTY);
  result.add_recycled_grid_generators(ggs);

  // Check whether we are using the widening-with-tokens technique
  // and there are still tokens available.
  if (tp != 0 && *tp > 0) {
    // There are tokens available.  If `result' is not a subset of
    // `x', then it is less precise and we use one of the available
    // tokens.
    if (!x.contains(result))
      --(*tp);
  }
  else
    // No tokens.
    x.m_swap(result);

  PPL_ASSERT(x.OK(true));
}

bool Parma_Polyhedra_Library::Grid::generators_are_minimized ( ) const

inlineprivate

Returns true if the system of generators is minimized.

Definition at line 55 of file Grid.inlines.hh.

References status, and Parma_Polyhedra_Library::Grid::Status::test_g_minimized().

Referenced by add_space_dimensions(), generator_widening_assign(), Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate(), quick_equivalence_test(), select_wider_generators(), and simplify_using_context_assign().

                                     {
  return status.test_g_minimized();
}

bool Parma_Polyhedra_Library::Grid::generators_are_up_to_date ( ) const

inlineprivate

Returns true if the system of generators is up-to-date.

Definition at line 45 of file Grid.inlines.hh.

References status, and Parma_Polyhedra_Library::Grid::Status::test_g_up_to_date().

Referenced by Parma_Polyhedra_Library::Box< ITV >::Box(), generator_widening_assign(), Grid(), Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate(), limited_congruence_extrapolation_assign(), limited_extrapolation_assign(), limited_generator_extrapolation_assign(), map_space_dimensions(), operator=(), time_elapse_assign(), upper_bound_assign(), and widening_assign().

                                      {
  return status.test_g_up_to_date();
}

const PPL::Grid_Generator_System & Parma_Polyhedra_Library::Grid::grid_generators ( ) const

Returns the system of generators.

Definition at line 311 of file Grid_public.cc.

References PPL_ASSERT, and set_empty().

Referenced by map_space_dimensions().

                               {
  if (space_dim == 0) {
    PPL_ASSERT(gen_sys.space_dimension() == 0
               && gen_sys.num_rows() == (marked_empty() ? 0U : 1U));
    return gen_sys;
  }

  if (marked_empty()) {
    PPL_ASSERT(gen_sys.has_no_rows());
    return gen_sys;
  }

  if (!generators_are_up_to_date() && !update_generators()) {
    // Updating found the grid empty.
    const_cast<Grid&>(*this).set_empty();
    return gen_sys;
  }

  return gen_sys;
}

int32_t Parma_Polyhedra_Library::Grid::hash_code ( ) const

inline

Returns a 32-bit hash code for *this.

If x and y are such that x == y, then x.hash_code() == y.hash_code().

Definition at line 234 of file Grid.inlines.hh.

References Parma_Polyhedra_Library::hash_code_from_dimension(), and space_dimension().

Referenced by Parma_Polyhedra_Library::Affine_Space::hash_code().

                      {
  return hash_code_from_dimension(space_dimension());
}

void Parma_Polyhedra_Library::Grid::intersection_assign ( const Grid & y )

Assigns to *this the intersection of *this and y.

Exceptions:

std::invalid_argument Thrown if *this and y are dimension-incompatible.

Definition at line 1390 of file Grid_public.cc.

References clear_congruences_minimized(), clear_generators_up_to_date(), con_sys, congruences_are_up_to_date(), Parma_Polyhedra_Library::Dense_Matrix::has_no_rows(), Parma_Polyhedra_Library::Congruence_System::insert(), marked_empty(), OK(), PPL_ASSERT, set_empty(), space_dim, and update_congruences().

Referenced by is_disjoint_from().

                                          {
  Grid& x = *this;
  // Dimension-compatibility check.
  if (x.space_dim != y.space_dim)
    throw_dimension_incompatible("intersection_assign(y)", "y", y);

  // If one of the two grids is empty, the intersection is empty.
  if (x.marked_empty())
    return;
  if (y.marked_empty()) {
    x.set_empty();
    return;
  }

  // If both grids are zero-dimensional, then at this point they are
  // necessarily universe, so the intersection is also universe.
  if (x.space_dim == 0)
    return;

  // The congruences must be up-to-date.
  if (!x.congruences_are_up_to_date())
    x.update_congruences();
  if (!y.congruences_are_up_to_date())
    y.update_congruences();

  if (!y.con_sys.has_no_rows()) {
    x.con_sys.insert(y.con_sys);
    // Grid_Generators may be out of date and congruences may have changed
    // from minimal form.
    x.clear_generators_up_to_date();
    x.clear_congruences_minimized();
  }

  PPL_ASSERT(x.OK() && y.OK());
}

bool Parma_Polyhedra_Library::Grid::is_bounded ( ) const

Returns true if and only if *this is bounded.

Definition at line 748 of file Grid_public.cc.

References Parma_Polyhedra_Library::Grid_Generator::is_line_or_parameter().

                          {
  // A zero-dimensional or empty grid is bounded.
  if (space_dim == 0
      || marked_empty()
      || (!generators_are_up_to_date() && !update_generators()))
    return true;

  // TODO: Consider using con_sys when gen_sys is out of date.

  if (gen_sys.num_rows() > 1) {
    // Check if all generators are the same point.
    const Grid_Generator& first_point = gen_sys[0];
    if (first_point.is_line_or_parameter())
      return false;
    for (dimension_type row = gen_sys.num_rows(); row-- > 0; ) {
      const Grid_Generator& gen = gen_sys[row];
      if (gen.is_line_or_parameter() || gen != first_point)
        return false;
    }
  }
  return true;
}

bool Parma_Polyhedra_Library::Grid::is_discrete ( ) const

Returns true if and only if *this is discrete.

A grid is discrete if it can be defined by a generator system which contains only points and parameters. This includes the empty grid and any grid in dimension zero.

Definition at line 772 of file Grid_public.cc.

                           {
  // A zero-dimensional or empty grid is discrete.
  if (space_dim == 0
      || marked_empty()
      || (!generators_are_up_to_date() && !update_generators()))
    return true;

  // Search for lines in the generator system.
  for (dimension_type row = gen_sys.num_rows(); row-- > 1; )
    if (gen_sys[row].is_line())
      return false;

  // The system of generators is composed only by
  // points and parameters: the grid is discrete.
  return true;
}

bool Parma_Polyhedra_Library::Grid::is_disjoint_from ( const Grid & y ) const

Returns true if and only if *this and y are disjoint.

Exceptions:

std::invalid_argument Thrown if x and y are dimension-incompatible.

Definition at line 2594 of file Grid_public.cc.

References intersection_assign(), is_empty(), and space_dim.

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PSET >::check_containment().

                                             {
  // Dimension-compatibility check.
  if (space_dim != y.space_dim)
    throw_dimension_incompatible("is_disjoint_from(y)", "y", y);
  Grid z = *this;
  z.intersection_assign(y);
  return z.is_empty();
}

bool Parma_Polyhedra_Library::Grid::is_empty ( ) const

Returns true if and only if *this is an empty grid.

Definition at line 695 of file Grid_public.cc.

References con_sys, dim_kinds, set_congruences_minimized(), set_empty(), and simplify().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PSET >::approximate_partition_aux(), Parma_Polyhedra_Library::Pointset_Powerset< PSET >::check_containment(), contains(), contains_integer_point(), is_disjoint_from(), operator<<(), operator==(), Parma_Polyhedra_Library::Pointset_Powerset< PSET >::Pointset_Powerset(), and simplify_using_context_assign().

                        {
  if (marked_empty())
    return true;
  // Try a fast-fail test: if generators are up-to-date then the
  // generator system (since it is well formed) contains a point.
  if (generators_are_up_to_date())
    return false;
  if (space_dim == 0)
    return false;
  if (congruences_are_minimized())
    // If the grid was empty it would be marked empty.
    return false;
  // Minimize the congruences to check if the grid is empty.
  Grid& gr = const_cast<Grid&>(*this);
  if (gr.simplify(gr.con_sys, gr.dim_kinds)) {
    gr.set_empty();
    return true;
  }
  gr.set_congruences_minimized();
  return false;
}

bool Parma_Polyhedra_Library::Grid::is_included_in ( const Grid & y ) const

private

Returns true if and only if *this is included in y.

Definition at line 237 of file Grid_nonpublic.cc.

References con_sys, congruences_are_minimized(), congruences_are_up_to_date(), marked_empty(), minimize(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), OK(), PPL_ASSERT, Parma_Polyhedra_Library::Congruence_System::satisfies_all_congruences(), space_dim, and update_congruences().

Referenced by contains(), operator==(), simplify_using_context_assign(), and upper_bound_assign_if_exact().

                                           {
  // Private method: the caller must ensure the following.
  PPL_ASSERT(space_dim == y.space_dim);
  PPL_ASSERT(!marked_empty() && !y.marked_empty() && space_dim > 0);

  const Grid& x = *this;

#if BE_LAZY
  if (!x.generators_are_up_to_date() && !x.update_generators())
    // Updating found `x' empty.
    return true;
  if (!y.congruences_are_up_to_date())
    y.update_congruences();
#else
  if (!x.generators_are_minimized() && !x.minimize())
    // Minimizing found `x' empty.
    return true;
  if (!y.congruences_are_minimized())
    y.minimize();
#endif

  PPL_ASSERT(x.OK());
  PPL_ASSERT(y.OK());

  const Grid_Generator_System& gs = x.gen_sys;
  const Congruence_System& cgs = y.con_sys;

  dimension_type num_rows = gs.num_rows();
  for (dimension_type i = num_rows; i-- > 0; )
    if (!cgs.satisfies_all_congruences(gs[i]))
      return false;

  // Inclusion holds.
  return true;
}

bool Parma_Polyhedra_Library::Grid::is_topologically_closed ( ) const

Returns true if and only if *this is a topologically closed subset of the vector space.

A grid is always topologically closed.

Definition at line 790 of file Grid_public.cc.

                                       {
  return true;
}

bool Parma_Polyhedra_Library::Grid::is_universe ( ) const

Returns true if and only if *this is a universe grid.

Definition at line 718 of file Grid_public.cc.

References PPL_ASSERT.

Referenced by operator<<().

                           {
  if (marked_empty())
    return false;

  if (space_dim == 0)
    return true;

  if (congruences_are_up_to_date()) {
    if (congruences_are_minimized())
      // The minimized universe congruence system has only one row,
      // the integrality congruence.
      return con_sys.num_rows() == 1 && con_sys[0].is_tautological();
  }
  else {
    update_congruences();
    return con_sys.num_rows() == 1 && con_sys[0].is_tautological();
  }

  // Test con_sys's inclusion in a universe generator system.

  // The zero dimension cases are handled above.
  Variable var(space_dim - 1);
  for (dimension_type i = space_dim; i-- > 0; )
    if (!con_sys.satisfies_all_congruences(grid_line(Variable(i) + var)))
      return false;
  PPL_ASSERT(con_sys.satisfies_all_congruences(grid_point(0*var)));
  return true;
}

void Parma_Polyhedra_Library::Grid::limited_congruence_extrapolation_assign	(	const Grid &	y,
		const Congruence_System &	cgs,
		unsigned *	tp = `NULL`
	)

Improves the result of the congruence variant of Grid widening computation by also enforcing those congruences in cgs that are satisfied by all the points of *this.

Parameters:

y	A grid that must be contained in `*this`;
cgs	The system of congruences used to improve the widened grid;
tp	An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique).

Exceptions:

std::invalid_argument Thrown if *this, y and cgs are dimension-incompatible.

Definition at line 151 of file Grid_widenings.cc.

References add_recycled_congruences(), congruence_widening_assign(), Parma_Polyhedra_Library::copy_contains(), generators_are_up_to_date(), Parma_Polyhedra_Library::Congruence_System::insert(), Parma_Polyhedra_Library::Poly_Con_Relation::is_included(), marked_empty(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), PPL_ASSERT, PPL_EXPECT_HEAVY, relation_with(), space_dim, Parma_Polyhedra_Library::Congruence_System::space_dimension(), update_generators(), and widening_assign().

                                                                 {
  Grid& x = *this;

  // Check dimension compatibility.
  if (x.space_dim != y.space_dim)
    throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
                                 "y", y);
  // `cgs' must be dimension-compatible with the two grids.
  const dimension_type cgs_space_dim = cgs.space_dimension();
  if (x.space_dim < cgs_space_dim)
    throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
                                 "cgs", cgs);

  const dimension_type cgs_num_rows = cgs.num_rows();
  // If `cgs' is empty (of rows), fall back to ordinary widening.
  if (cgs_num_rows == 0) {
    x.widening_assign(y, tp);
    return;
  }

  // Assume `y' is contained in or equal to `x'.
  PPL_EXPECT_HEAVY(copy_contains(x, y));

  if (y.marked_empty())
    return;
  if (x.marked_empty())
    return;

  // The limited widening between two grids in a zero-dimensional
  // space is also a grid in a zero-dimensional space.
  if (x.space_dim == 0)
    return;

  // Update the generators of `x': these are used to select, from the
  // congruences in `cgs', those that must be added to the widened
  // grid.
  if (!x.generators_are_up_to_date() && !x.update_generators())
    // `x' is empty.
    return;

  if (tp == NULL || *tp == 0) {
    // Widening may change the grid, so add the congruences.
    Congruence_System new_cgs;
    // The congruences to be added need only be satisfied by all the
    // generators of `x', as `y <= x'.  Iterate upwards here, to keep
    // the relative ordering of congruences (just for aesthetics).
    for (dimension_type i = 0; i < cgs_num_rows; ++i) {
      const Congruence& cg = cgs[i];
      if (x.relation_with(cg) == Poly_Con_Relation::is_included())
        new_cgs.insert(cg);
    }
    x.congruence_widening_assign(y, tp);
    x.add_recycled_congruences(new_cgs);
  }
  else
    // There are tokens, so widening will leave the grid the same.
    x.congruence_widening_assign(y, tp);

  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::limited_extrapolation_assign	(	const Grid &	y,
		const Congruence_System &	cgs,
		unsigned *	tp = `NULL`
	)

Improves the result of the Grid widening computation by also enforcing those congruences in cgs that are satisfied by all the points of *this.

Parameters:

y	A grid that must be contained in `*this`;
cgs	The system of congruences used to improve the widened grid;
tp	An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique).

Exceptions:

std::invalid_argument Thrown if *this, y and cgs are dimension-incompatible.

Definition at line 433 of file Grid_widenings.cc.

References add_recycled_congruences(), Parma_Polyhedra_Library::copy_contains(), generators_are_up_to_date(), Parma_Polyhedra_Library::Congruence_System::insert(), Parma_Polyhedra_Library::Poly_Con_Relation::is_included(), marked_empty(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), PPL_ASSERT, PPL_EXPECT_HEAVY, relation_with(), space_dim, Parma_Polyhedra_Library::Congruence_System::space_dimension(), update_generators(), and widening_assign().

                                                      {
  Grid& x = *this;

  // Check dimension compatibility.
  if (x.space_dim != y.space_dim)
    throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
                                 "y", y);
  // `cgs' must be dimension-compatible with the two grids.
  const dimension_type cgs_space_dim = cgs.space_dimension();
  if (x.space_dim < cgs_space_dim)
    throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
                                 "cgs", cgs);

  const dimension_type cgs_num_rows = cgs.num_rows();
  // If `cgs' is empty (of rows), fall back to ordinary widening.
  if (cgs_num_rows == 0) {
    x.widening_assign(y, tp);
    return;
  }

  // Assume `y' is contained in or equal to `x'.
  PPL_EXPECT_HEAVY(copy_contains(x, y));

  if (y.marked_empty())
    return;
  if (x.marked_empty())
    return;

  // The limited widening between two grids in a zero-dimensional
  // space is also a grid in a zero-dimensional space.
  if (x.space_dim == 0)
    return;

  // Update the generators of `x': these are used to select, from the
  // congruences in `cgs', those that must be added to the widened
  // grid.
  if (!x.generators_are_up_to_date() && !x.update_generators())
    // `x' is empty.
    return;

  if (tp == NULL || *tp == 0) {
    // Widening may change the grid, so add the congruences.
    Congruence_System new_cgs;
    // The congruences to be added need only be satisfied by all the
    // generators of `x', as `y <= x'.  Iterate upwards here, to keep
    // the relative ordering of congruences (just for aesthetics).
    for (dimension_type i = 0; i < cgs_num_rows; ++i) {
      const Congruence& cg = cgs[i];
      if (x.relation_with(cg) == Poly_Con_Relation::is_included())
        new_cgs.insert(cg);
    }
    x.widening_assign(y, tp);
    x.add_recycled_congruences(new_cgs);
  }
  else
    // There are tokens, so widening will leave the grid the same.
    x.widening_assign(y, tp);

  PPL_ASSERT(OK());
}

void Parma_Polyhedra_Library::Grid::limited_generator_extrapolation_assign	(	const Grid &	y,
		const Congruence_System &	cgs,
		unsigned *	tp = `NULL`
	)

Improves the result of the generator variant of the Grid widening computation by also enforcing those congruences in cgs that are satisfied by all the points of *this.

Parameters:

y	A grid that must be contained in `*this`;
cgs	The system of congruences used to improve the widened grid;
tp	An optional pointer to an unsigned variable storing the number of available tokens (to be used when applying the widening with tokens delay technique).

Exceptions:

std::invalid_argument Thrown if *this, y and cgs are dimension-incompatible.

Definition at line 341 of file Grid_widenings.cc.

References add_recycled_congruences(), Parma_Polyhedra_Library::copy_contains(), generator_widening_assign(), generators_are_up_to_date(), Parma_Polyhedra_Library::Congruence_System::insert(), Parma_Polyhedra_Library::Poly_Con_Relation::is_included(), marked_empty(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), PPL_ASSERT, PPL_EXPECT_HEAVY, relation_with(), space_dim, Parma_Polyhedra_Library::Congruence_System::space_dimension(), and update_generators().

                                                                {
  Grid& x = *this;

  // Check dimension compatibility.
  if (x.space_dim != y.space_dim)
    throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
                                 "y", y);
  // `cgs' must be dimension-compatible with the two grids.
  const dimension_type cgs_space_dim = cgs.space_dimension();
  if (x.space_dim < cgs_space_dim)
    throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
                                 "cgs", cgs);

  const dimension_type cgs_num_rows = cgs.num_rows();
  // If `cgs' is empty (of rows), fall back to ordinary widening.
  if (cgs_num_rows == 0) {
    x.generator_widening_assign(y, tp);
    return;
  }

  // Assume `y' is contained in or equal to `x'.
  PPL_EXPECT_HEAVY(copy_contains(x, y));

  if (y.marked_empty())
    return;
  if (x.marked_empty())
    return;

  // The limited widening between two grids in a zero-dimensional
  // space is also a grid in a zero-dimensional space.
  if (x.space_dim == 0)
    return;

  // Update the generators of `x': these are used to select, from the
  // congruences in `cgs', those that must be added to the widened
  // grid.
  if (!x.generators_are_up_to_date() && !x.update_generators())
    // `x' is empty.
    return;

  if (tp == NULL || *tp == 0) {
    // Widening may change the grid, so add the congruences.
    Congruence_System new_cgs;
    // The congruences to be added need only be satisfied by all the
    // generators of `x', as `y <= x'.  Iterate upwards here, to keep
    // the relative ordering of congruences (just for aesthetics).
    for (dimension_type i = 0; i < cgs_num_rows; ++i) {
      const Congruence& cg = cgs[i];
      if (x.relation_with(cg) == Poly_Con_Relation::is_included())
        new_cgs.insert(cg);
    }
    x.generator_widening_assign(y, tp);
    x.add_recycled_congruences(new_cgs);
  }
  else
    // There are tokens, so widening will leave the grid the same.
    x.generator_widening_assign(y, tp);

  PPL_ASSERT(OK());
}

bool Parma_Polyhedra_Library::Grid::lower_triangular	(	const Congruence_System &	sys,
		const Dimension_Kinds &	dim_kinds
	)

staticprivate

If sys is lower triangular return true, else return false.

Definition at line 37 of file Grid_conversion.cc.

References CON_VIRTUAL, Parma_Polyhedra_Library::Dense_Matrix::num_columns(), and Parma_Polyhedra_Library::Dense_Matrix::num_rows().

Referenced by conversion().

                                                         {
  const dimension_type num_columns = sys.num_columns() - 1;

  // Check for easy square failure case.
  if (sys.num_rows() > num_columns)
    return false;

  // Check triangularity.

  dimension_type row = 0;
  for (dimension_type dim = num_columns; dim-- > 0; ) {
    if (dim_kinds[dim] == CON_VIRTUAL)
      continue;
    const Congruence& cg = sys[row];
    ++row;
    // Check diagonal.
    if (cg[dim] <= 0)
      return false;
    // Check elements following diagonal.
    dimension_type col = dim;
    while (++col < num_columns)
      if (cg[col] != 0)
        return false;
  }

  // Check squareness.
  return row == sys.num_rows();
}

void Parma_Polyhedra_Library::Grid::m_swap ( Grid & y )

inline

Swaps *this with grid y. (*this and y can be dimension-incompatible.)

Definition at line 249 of file Grid.inlines.hh.

References con_sys, dim_kinds, gen_sys, space_dim, status, and swap().

Referenced by Parma_Polyhedra_Library::Affine_Space::Affine_Space(), congruence_widening_assign(), generator_widening_assign(), map_space_dimensions(), simplify_using_context_assign(), and swap().

                    {
  using std::swap;
  swap(con_sys, y.con_sys);
  swap(gen_sys, y.gen_sys);
  swap(status, y.status);
  swap(space_dim, y.space_dim);
  swap(dim_kinds, y.dim_kinds);
}

template<typename Partial_Function >

void Parma_Polyhedra_Library::Grid::map_space_dimensions ( const Partial_Function & pfunc )

Remaps the dimensions of the vector space according to a partial function.

If pfunc maps only some of the dimensions of *this then the rest will be projected away.

If the highest dimension mapped to by pfunc is higher than the highest dimension in *this then the number of dimensions in *this will be increased to the highest dimension mapped to by pfunc.

Parameters:

pfunc The partial function specifying the destiny of each space dimension.

The template type parameter Partial_Function must provide the following methods.

      bool has_empty_codomain() const

returns true if and only if the represented partial function has an empty codomain (i.e., it is always undefined). The has_empty_codomain() method will always be called before the methods below. However, if has_empty_codomain() returns true, none of the functions below will be called.

      dimension_type max_in_codomain() const

returns the maximum value that belongs to the codomain of the partial function. The max_in_codomain() method is called at most once.

      bool maps(dimension_type i, dimension_type& j) const

Let $f$ be the represented function and $k$ be the value of i. If $f$ is defined in $k$ , then $f(k)$ is assigned to j and true is returned. If $f$ is undefined in $k$ , then false is returned. This method is called at most $n$ times, where $n$ is the dimension of the vector space enclosing the grid.

The result is undefined if pfunc does not encode a partial function with the properties described in the specification of the mapping operator.

Definition at line 112 of file Grid.templates.hh.

                                                        {
  if (space_dim == 0)
    return;

  if (pfunc.has_empty_codomain()) {
    // All dimensions vanish: the grid becomes zero_dimensional.
    if (marked_empty()
        || (!generators_are_up_to_date() && !update_generators())) {
      // Removing all dimensions from the empty grid.
      space_dim = 0;
      set_empty();
    }
    else
      // Removing all dimensions from a non-empty grid.
      set_zero_dim_univ();

    PPL_ASSERT(OK());
    return;
  }

  dimension_type new_space_dimension = pfunc.max_in_codomain() + 1;

  if (new_space_dimension == space_dim) {
    // The partial function `pfunc' is indeed total and thus specifies
    // a permutation, that is, a renaming of the dimensions.  For
    // maximum efficiency, we will simply permute the columns of the
    // constraint system and/or the generator system.

    // We first compute suitable permutation cycles for the columns of
    // the `con_sys' and `gen_sys' matrices.  We will represent them
    // with a linear array, using 0 as a terminator for each cycle
    // (notice that the columns with index 0 of `con_sys' and
    // `gen_sys' represent the inhomogeneous terms, and thus are
    // unaffected by the permutation of dimensions).
    // Cycles of length 1 will be omitted so that, in the worst case,
    // we will have `space_dim' elements organized in `space_dim/2'
    // cycles, which means we will have at most `space_dim/2'
    // terminators.
    std::vector<dimension_type> cycles;
    cycles.reserve(space_dim + space_dim/2);

    // Used to mark elements as soon as they are inserted in a cycle.
    std::deque<bool> visited(space_dim);

    for (dimension_type i = space_dim; i-- > 0; ) {
      if (!visited[i]) {
        dimension_type j = i;
        do {
          visited[j] = true;
          // The following initialization is only to make the compiler happy.
          dimension_type k = 0;
          if (!pfunc.maps(j, k))
            throw_invalid_argument("map_space_dimensions(pfunc)",
                                   " pfunc is inconsistent");
          if (k == j)
            // Cycle of length 1: skip it.
            goto skip;

          cycles.push_back(j+1);
          // Go along the cycle.
          j = k;
        } while (!visited[j]);
        // End of cycle: mark it.
        cycles.push_back(0);
      skip:
        ;
      }
    }

    // If `cycles' is empty then `pfunc' is the identity.
    if (cycles.empty())
      return;

    // Permute all that is up-to-date.
    if (congruences_are_up_to_date()) {
      con_sys.permute_columns(cycles);
      clear_congruences_minimized();
    }

    if (generators_are_up_to_date()) {
      gen_sys.permute_columns(cycles);
      clear_generators_minimized();
    }

    PPL_ASSERT(OK());
    return;
  }

  // If control gets here, then `pfunc' is not a permutation and some
  // dimensions must be projected away.

  const Grid_Generator_System& old_gensys = grid_generators();

  if (old_gensys.has_no_rows()) {
    // The grid is empty.
    Grid new_grid(new_space_dimension, EMPTY);
    m_swap(new_grid);
    PPL_ASSERT(OK());
    return;
  }

  // Make a local copy of the partial function.
  std::vector<dimension_type> pfunc_maps(space_dim, not_a_dimension());
  for (dimension_type j = space_dim; j-- > 0; ) {
    dimension_type pfunc_j;
    if (pfunc.maps(j, pfunc_j))
      pfunc_maps[j] = pfunc_j;
  }

  Grid_Generator_System new_gensys;
  // Set sortedness, for the assertion met via gs::insert.
  new_gensys.set_sorted(false);
  // Get the divisor of the first point.
  Grid_Generator_System::const_iterator i;
  Grid_Generator_System::const_iterator old_gensys_end = old_gensys.end();
  for (i = old_gensys.begin(); i != old_gensys_end; ++i)
    if (i->is_point())
      break;
  PPL_ASSERT(i != old_gensys_end);
  const Coefficient& system_divisor = i->divisor();
  for (i = old_gensys.begin(); i != old_gensys_end; ++i) {
    const Grid_Generator& old_g = *i;
    Linear_Expression e(0 * Variable(new_space_dimension-1));
    bool all_zeroes = true;
    for (dimension_type j = space_dim; j-- > 0; ) {
      if (old_g.coefficient(Variable(j)) != 0
          && pfunc_maps[j] != not_a_dimension()) {
        e += Variable(pfunc_maps[j]) * old_g.coefficient(Variable(j));
        all_zeroes = false;
      }
    }
    switch (old_g.type()) {
    case Grid_Generator::LINE:
      if (!all_zeroes)
        new_gensys.insert(grid_line(e));
      break;
    case Grid_Generator::PARAMETER:
      if (!all_zeroes)
        new_gensys.insert(parameter(e, system_divisor));
      break;
    case Grid_Generator::POINT:
      new_gensys.insert(grid_point(e, old_g.divisor()));
      break;
    }
  }

  Grid new_grid(new_gensys);
  m_swap(new_grid);

  PPL_ASSERT(OK(true));
}

bool Parma_Polyhedra_Library::Grid::marked_empty ( ) const

inlineprivate

Returns true if the grid is known to be empty.

The return value false does not necessarily implies that *this is non-empty.

Definition at line 35 of file Grid.inlines.hh.

References status, and Parma_Polyhedra_Library::Grid::Status::test_empty().

Referenced by add_congruence(), add_congruences(), add_constraint(), Parma_Polyhedra_Library::Box< ITV >::Box(), concatenate_assign(), congruence_widening_assign(), contains(), difference_assign(), generator_widening_assign(), Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate(), intersection_assign(), is_included_in(), limited_congruence_extrapolation_assign(), limited_extrapolation_assign(), limited_generator_extrapolation_assign(), map_space_dimensions(), operator=(), operator==(), quick_equivalence_test(), select_wider_congruences(), select_wider_generators(), time_elapse_assign(), upper_bound_assign(), and upper_bound_assign_if_exact().

                         {
  return status.test_empty();
}

bool Parma_Polyhedra_Library::Grid::max_min	(	const Linear_Expression &	expr,
		const char *	method_call,
		Coefficient &	ext_n,
		Coefficient &	ext_d,
		bool &	included,
		Generator *	point = `NULL`
	)		const

private

Maximizes or minimizes expr subject to *this.

Parameters:

expr	The linear expression to be maximized or minimized subject to `*this`;
method_call	The call description of the public parent method, for example "maximize(e)". Passed to throw_dimension_incompatible, as the first argument;
ext_n	The numerator of the extremum value;
ext_d	The denominator of the extremum value;
included	`true` if and only if the extremum of `expr` in `*this` can actually be reached (which is always the case);
point	When maximization or minimization succeeds, will be assigned the point where `expr` reaches the extremum value.

Exceptions:

std::invalid_argument Thrown if expr and *this are dimension-incompatible.

If *this is empty or expr is not bounded in the appropriate direction, false is returned and ext_n, ext_d, included and point are left untouched.

Definition at line 393 of file Grid_nonpublic.cc.

References Parma_Polyhedra_Library::Grid_Generator::coefficient(), dim_kinds, Parma_Polyhedra_Library::Grid_Generator::divisor(), Parma_Polyhedra_Library::exact_div_assign(), Parma_Polyhedra_Library::gcd_assign(), gen_sys, Parma_Polyhedra_Library::Scalar_Products::homogeneous_assign(), Parma_Polyhedra_Library::Linear_Expression::inhomogeneous_term(), Parma_Polyhedra_Library::Generator::point(), PPL_DIRTY_TEMP_COEFFICIENT, set_generators_minimized(), and simplify().

Referenced by maximize(), and minimize().

                                           {
  if (bounds(expr, method_call)) {
    if (marked_empty())
      return false;
    if (space_dim == 0) {
      ext_n = 0;
      ext_d = 1;
      included = true;
      if (point != 0)
        *point = Generator::point();
      return true;
    }
    // Grid::bounds above ensures the generators are up to date.
    if (!generators_are_minimized()) {
      // Minimize the generator system.
      Grid& gr = const_cast<Grid&>(*this);
      gr.simplify(gr.gen_sys, gr.dim_kinds);
      gr.set_generators_minimized();
    }

    const Grid_Generator& gen = gen_sys[0];
    Scalar_Products::homogeneous_assign(ext_n, expr, gen);
    ext_n += expr.inhomogeneous_term();
    ext_d = gen.divisor();
    // Reduce ext_n and ext_d.
    PPL_DIRTY_TEMP_COEFFICIENT(gcd);
    gcd_assign(gcd, ext_n, ext_d);
    exact_div_assign(ext_n, ext_n, gcd);
    exact_div_assign(ext_d, ext_d, gcd);

    included = true;
    if (point != 0) {
      Linear_Expression e;
      for (dimension_type i = space_dim; i-- > 0; )
        e += gen.coefficient(Variable(i)) * Variable(i);
      *point = Generator::point(e, gen.divisor());
    }
    return true;
  }
  return false;
}

dimension_type Parma_Polyhedra_Library::Grid::max_space_dimension ( )

inlinestatic

Returns the maximum space dimension all kinds of Grid can handle.

Definition at line 111 of file Grid.inlines.hh.

References Parma_Polyhedra_Library::Congruence_System::max_space_dimension(), and Parma_Polyhedra_Library::Grid_Generator_System::max_space_dimension().

Referenced by Grid(), and Parma_Polyhedra_Library::max_space_dimension().

                          {
  // One dimension is reserved to have a value of type dimension_type
  // that does not represent a legal dimension.
  return std::min(std::numeric_limits<dimension_type>::max() - 1,
                  std::min(Congruence_System::max_space_dimension(),
                           Grid_Generator_System::max_space_dimension()
                           )
                  );
}

bool Parma_Polyhedra_Library::Grid::maximize	(	const Linear_Expression &	expr,
		Coefficient &	sup_n,
		Coefficient &	sup_d,
		bool &	maximum
	)		const

inline

Returns true if and only if *this is not empty and expr is bounded from above in *this, in which case the supremum value is computed.

Parameters:

expr	The linear expression to be maximized subject to `*this`;
sup_n	The numerator of the supremum value;
sup_d	The denominator of the supremum value;
maximum	`true` if the supremum value can be reached in `this`. Always `true` when `this` bounds `expr`. Present for interface compatibility with class Polyhedron, where closure points can result in a value of false.

Exceptions:

std::invalid_argument Thrown if expr and *this are dimension-incompatible.

If *this is empty or expr is not bounded by *this, false is returned and sup_n, sup_d and maximum are left untouched.

Definition at line 327 of file Grid.inlines.hh.

References max_min().

Referenced by Parma_Polyhedra_Library::Box< ITV >::Box(), and Parma_Polyhedra_Library::Affine_Space::maximize().

                                                                            {
  return max_min(expr, "maximize(e, ...)", sup_n, sup_d, maximum);
}

bool Parma_Polyhedra_Library::Grid::maximize	(	const Linear_Expression &	expr,
		Coefficient &	sup_n,
		Coefficient &	sup_d,
		bool &	maximum,
		Generator &	point
	)		const

inline

Returns true if and only if *this is not empty and expr is bounded from above in *this, in which case the supremum value and a point where expr reaches it are computed.

Parameters:

expr	The linear expression to be maximized subject to `*this`;
sup_n	The numerator of the supremum value;
sup_d	The denominator of the supremum value;
maximum	`true` if the supremum value can be reached in `this`. Always `true` when `this` bounds `expr`. Present for interface compatibility with class Polyhedron, where closure points can result in a value of false;
point	When maximization succeeds, will be assigned a point where `expr` reaches its supremum value.

Exceptions:

std::invalid_argument Thrown if expr and *this are dimension-incompatible.

If *this is empty or expr is not bounded by *this, false is returned and sup_n, sup_d, maximum and point are left untouched.

Definition at line 333 of file Grid.inlines.hh.

References max_min().

                                       {
  return max_min(expr, "maximize(e, ...)", sup_n, sup_d, maximum, &point);
}

bool Parma_Polyhedra_Library::Grid::minimize	(	const Linear_Expression &	expr,
		Coefficient &	inf_n,
		Coefficient &	inf_d,
		bool &	minimum
	)		const

inline

Returns true if and only if *this is not empty and expr is bounded from below in *this, in which case the infimum value is computed.

Parameters:

expr	The linear expression to be minimized subject to `*this`;
inf_n	The numerator of the infimum value;
inf_d	The denominator of the infimum value;
minimum	`true` if the is the infimum value can be reached in `this`. Always `true` when `this` bounds `expr`. Present for interface compatibility with class Polyhedron, where closure points can result in a value of false.

Exceptions:

std::invalid_argument Thrown if expr and *this are dimension-incompatible.

If *this is empty or expr is not bounded from below, false is returned and inf_n, inf_d and minimum are left untouched.

Definition at line 340 of file Grid.inlines.hh.

References max_min().

Referenced by is_included_in(), Parma_Polyhedra_Library::Affine_Space::minimize(), and simplify_using_context_assign().

                                                                            {
  return max_min(expr, "minimize(e, ...)", inf_n, inf_d, minimum);
}

bool Parma_Polyhedra_Library::Grid::minimize	(	const Linear_Expression &	expr,
		Coefficient &	inf_n,
		Coefficient &	inf_d,
		bool &	minimum,
		Generator &	point
	)		const

inline

Returns true if and only if *this is not empty and expr is bounded from below in *this, in which case the infimum value and a point where expr reaches it are computed.

Parameters:

expr	The linear expression to be minimized subject to `*this`;
inf_n	The numerator of the infimum value;
inf_d	The denominator of the infimum value;
minimum	`true` if the is the infimum value can be reached in `this`. Always `true` when `this` bounds `expr`. Present for interface compatibility with class Polyhedron, where closure points can result in a value of false;
point	When minimization succeeds, will be assigned a point where `expr` reaches its infimum value.

Exceptions:

std::invalid_argument Thrown if expr and *this are dimension-incompatible.

If *this is empty or expr is not bounded from below, false is returned and inf_n, inf_d, minimum and point are left untouched.

Definition at line 346 of file Grid.inlines.hh.

References max_min().

                                       {
  return max_min(expr, "minimize(e, ...)", inf_n, inf_d, minimum, &point);
}

bool Parma_Polyhedra_Library::Grid::minimize ( ) const

private

Minimizes both the congruences and the generators.

Returns:: false if and only if *this turns out to be an empty grid.

Minimization is performed on each system only if the minimized Status field is clear.

Definition at line 515 of file Grid_nonpublic.cc.

References con_sys, dim_kinds, Parma_Polyhedra_Library::Implementation::BD_Shapes::empty, gen_sys, PPL_ASSERT, set_congruences_minimized(), set_generators_minimized(), and simplify().

                        {
  // 0-dimension and empty grids are already minimized.
  if (marked_empty())
    return false;
  if (space_dim == 0)
    return true;

  // Are both systems already minimized?
  if (congruences_are_minimized() && generators_are_minimized())
    return true;

  // Invoke update_generators, update_congruences or simplify,
  // depending on the state of the systems.
  if (congruences_are_up_to_date()) {
    if (generators_are_up_to_date()) {
      Grid& gr = const_cast<Grid&>(*this);
      // Only one of the systems can be minimized here.
      if (congruences_are_minimized()) {
        // Minimize the generator system.
        gr.simplify(gr.gen_sys, gr.dim_kinds);
        gr.set_generators_minimized();
      }
      else {
#ifndef NDEBUG
        // Both systems are up to date, and the empty case is handled
        // above, so the grid should contain points.
        bool empty = simplify(gr.con_sys, gr.dim_kinds);
        PPL_ASSERT(!empty);
#else
        simplify(gr.con_sys, gr.dim_kinds);
#endif
        gr.set_congruences_minimized();
        if (!generators_are_minimized()) {
          // Minimize the generator system.
          gr.simplify(gr.gen_sys, gr.dim_kinds);
          gr.set_generators_minimized();
        }
      }
    }
    else {
      // Updating the generators may reveal that `*this' is empty.
      const bool ret = update_generators();
      PPL_ASSERT(OK());
      return ret;
    }
  }
  else {
    PPL_ASSERT(generators_are_up_to_date());
    update_congruences();
  }
  PPL_ASSERT(OK());
  return true;
}

const PPL::Congruence_System & Parma_Polyhedra_Library::Grid::minimized_congruences ( ) const

Returns the system of congruences in minimal form.

Definition at line 298 of file Grid_public.cc.

References con_sys, dim_kinds, set_congruences_minimized(), set_empty(), and simplify().

Referenced by Parma_Polyhedra_Library::Pointset_Powerset< PSET >::approximate_partition(), Parma_Polyhedra_Library::BD_Shape< T >::BD_Shape(), Parma_Polyhedra_Library::Partially_Reduced_Product< D1, D2, R >::minimized_congruences(), minimized_constraints(), Parma_Polyhedra_Library::Octagonal_Shape< T >::Octagonal_Shape(), and operator<<().

                                     {
  if (congruences_are_up_to_date() && !congruences_are_minimized()) {
    // Minimize the congruences.
    Grid& gr = const_cast<Grid&>(*this);
    if (gr.simplify(gr.con_sys, gr.dim_kinds))
      gr.set_empty();
    else
      gr.set_congruences_minimized();
  }
  return congruences();
}

Constraint_System Parma_Polyhedra_Library::Grid::minimized_constraints ( ) const

inline

Returns a minimal system of equality constraints satisfied by *this with the same affine dimension as *this.

Definition at line 244 of file Grid.inlines.hh.

References minimized_congruences().

Referenced by Parma_Polyhedra_Library::Affine_Space::minimized_constraints().

                                  {
  return Constraint_System(minimized_congruences());
}

const PPL::Grid_Generator_System & Parma_Polyhedra_Library::Grid::minimized_grid_generators ( ) const

Returns the minimized system of generators.

Definition at line 333 of file Grid_public.cc.

References dim_kinds, gen_sys, PPL_ASSERT, set_empty(), set_generators_minimized(), and simplify().

                                         {
  if (space_dim == 0) {
    PPL_ASSERT(gen_sys.space_dimension() == 0
               && gen_sys.num_rows() == (marked_empty() ? 0U : 1U));
    return gen_sys;
  }

  if (marked_empty()) {
    PPL_ASSERT(gen_sys.has_no_rows());
    return gen_sys;
  }

  if (generators_are_up_to_date()) {
    if (!generators_are_minimized()) {
      // Minimize the generators.
      Grid& gr = const_cast<Grid&>(*this);
      gr.simplify(gr.gen_sys, gr.dim_kinds);
      gr.set_generators_minimized();
    }
  }
  else if (!update_generators()) {
    // Updating found the grid empty.
    const_cast<Grid&>(*this).set_empty();
    return gen_sys;
  }

  return gen_sys;
}

void Parma_Polyhedra_Library::Grid::multiply_grid	(	const Coefficient &	multiplier,
		Congruence &	cg,
		Congruence_System &	dest,
		dimension_type	num_rows,
		dimension_type	num_dims
	)

staticprivate

Multiply the elements of dest by multiplier.

Definition at line 127 of file Grid_conversion.cc.

References Parma_Polyhedra_Library::Congruence::is_equality(), Parma_Polyhedra_Library::Congruence::is_proper_congruence(), and PPL_ASSERT.

Referenced by conversion().

                                                   {
  if (multiplier == 1)
    return;

  if (cg.is_proper_congruence())
    // Multiply every element of every congruence.
    for (dimension_type index = num_rows; index-- > 0; ) {
      Congruence& congruence = dest[index];
      if (congruence.is_proper_congruence())
        for (dimension_type column = num_dims; column-- > 0; )
          congruence[column] *= multiplier;
    }
  else {
    PPL_ASSERT(cg.is_equality());
    // Multiply every element of the equality.
    for (dimension_type column = num_dims; column-- > 0; )
      cg[column] *= multiplier;
  }
}

void Parma_Polyhedra_Library::Grid::multiply_grid	(	const Coefficient &	multiplier,
		Grid_Generator &	gen,
		Grid_Generator_System &	dest,
		dimension_type	num_rows,
		dimension_type	num_dims
	)

staticprivate

Multiply the elements of dest by multiplier.

Definition at line 104 of file Grid_conversion.cc.

References Parma_Polyhedra_Library::Grid_Generator::is_line(), Parma_Polyhedra_Library::Grid_Generator::is_parameter_or_point(), and PPL_ASSERT.

                                                   {
  if (multiplier == 1)
    return;

  if (gen.is_line())
    // Multiply every element of the line.
    for (dimension_type column = num_dims; column-- > 0; )
      gen[column] *= multiplier;
  else {
    PPL_ASSERT(gen.is_parameter_or_point());
    // Multiply every element of every parameter.
    for (dimension_type index = num_rows; index-- > 0; ) {
      Grid_Generator& generator = dest[index];
      if (generator.is_parameter_or_point())
        for (dimension_type column = num_dims; column-- > 0; )
          generator[column] *= multiplier;
    }
  }
}

void Parma_Polyhedra_Library::Grid::normalize_divisors	(	Grid_Generator_System &	sys,
		Coefficient &	divisor,
		const Grid_Generator *	first_point = `NULL`
	)

staticprivate

Normalizes the divisors in sys.

Converts sys to an equivalent system in which the divisors are of equal value.

Parameters:

sys	The generator system to be normalized. It must have at least one row.
divisor	A reference to the initial value of the divisor. The resulting value of this object is the new system divisor.
first_point	If `first_point` has a value other than NULL then it is taken as the first point in `sys`, and it is assumed that any following points have the same divisor as `first_point`.

Definition at line 610 of file Grid_nonpublic.cc.

References Parma_Polyhedra_Library::Grid_Generator::divisor(), Parma_Polyhedra_Library::Grid_Generator::is_parameter_or_point(), Parma_Polyhedra_Library::lcm_assign(), Parma_Polyhedra_Library::Grid_Generator_System::num_rows(), PPL_ASSERT, and Parma_Polyhedra_Library::Grid_Generator_System::space_dimension().

Referenced by normalize_divisors().

                                                                 {
  PPL_ASSERT(divisor >= 0);
  if (sys.space_dimension() > 0 && divisor > 0) {
    dimension_type row = 0;
    dimension_type num_rows = sys.num_rows();

    if (first_point != 0)
      lcm_assign(divisor, divisor, (*first_point).divisor());
    else {
      PPL_ASSERT(num_rows > 0);
      // Move to the first point or parameter.
      while (sys[row].is_line())
        if (++row == num_rows)
          // All rows are lines.
          return;

      // Calculate the LCM of the given divisor and the divisor of
      // every point or parameter.
      while (row < num_rows) {
        const Grid_Generator& g = sys[row];
        if (g.is_parameter_or_point())
          lcm_assign(divisor, divisor, g.divisor());
        ++row;
      }
    }

    // Represent every point and every parameter using the newly
    // calculated divisor.
    for (row = num_rows; row-- > 0; )
      sys[row].scale_to_divisor(divisor);
  }
}

void Parma_Polyhedra_Library::Grid::normalize_divisors ( Grid_Generator_System & sys )

inlinestaticprivate

Normalizes the divisors in sys.

Converts sys to an equivalent system in which the divisors are of equal value.

Parameters:

sys	The generator system to be normalized. It must have at least one row.

Definition at line 353 of file Grid.inlines.hh.

References normalize_divisors(), and PPL_DIRTY_TEMP_COEFFICIENT.

                                                   {
  PPL_DIRTY_TEMP_COEFFICIENT(divisor);
  divisor = 1;
  normalize_divisors(sys, divisor);
}

void Parma_Polyhedra_Library::Grid::normalize_divisors	(	Grid_Generator_System &	sys,
		Grid_Generator_System &	gen_sys
	)

staticprivate

Normalize all the divisors in sys and gen_sys.

Modify sys and gen_sys to use the same single divisor value for all generators, leaving each system representing the grid it represented originally.

Parameters:

sys	The first of the generator systems to be normalized.
gen_sys	The second of the generator systems to be normalized. This system must have at least one row and the divisors of the generators in this system must be equal.

Exceptions:

std::runtime_error Thrown if all rows in gen_sys are lines and/or parameters.

Definition at line 570 of file Grid_nonpublic.cc.

References Parma_Polyhedra_Library::Grid_Generator::divisor(), Parma_Polyhedra_Library::Grid_Generator::is_parameter_or_point(), Parma_Polyhedra_Library::Grid_Generator_System::num_rows(), PPL_ASSERT, and PPL_DIRTY_TEMP_COEFFICIENT.

                                                              {
#ifndef NDEBUG
  const dimension_type num_rows = gen_sys.num_rows();
#endif
  PPL_ASSERT(num_rows > 0);

  // Find the first point in gen_sys.
  dimension_type row = 0;
  while (gen_sys[row].is_line_or_parameter()) {
    ++row;
    // gen_sys should have at least one point.
    PPL_ASSERT(row < num_rows);
  }
  Grid_Generator& first_point = gen_sys[row];
  const Coefficient& gen_sys_divisor = first_point.divisor();

#ifndef NDEBUG
  // Check that the divisors in gen_sys are equal.
  for (dimension_type i = row + 1; i < num_rows; ++i) {
    Grid_Generator& g = gen_sys[i];
    if (g.is_parameter_or_point())
      PPL_ASSERT(gen_sys_divisor == g.divisor());
  }
#endif // !defined(NDEBUG)

  PPL_DIRTY_TEMP_COEFFICIENT(divisor);
  divisor = gen_sys_divisor;
  // Adjust sys to include the gen_sys divisor.
  normalize_divisors(sys, divisor);
  if (divisor != gen_sys_divisor)
    // Adjust gen_sys to use the new divisor.
    //
    // The points and parameters in gen_sys share a common divisor
    // value, so the new divisor will be the LCM of this common
    // divisor and `divisor', hence the third argument.
    normalize_divisors(gen_sys, divisor, &first_point);
}

bool Parma_Polyhedra_Library::Grid::OK ( bool check_not_empty = false ) const

Checks if all the invariants are satisfied.

Returns:: true if and only if *this satisfies all the invariants and either check_not_empty is false or *this is not empty.

Parameters:

check_not_empty true if and only if, in addition to checking the invariants, *this must be checked to be not empty.

The check is performed so as to intrude as little as possible. If the library has been compiled with run-time assertions enabled, error messages are written on std::cerr in case invariants are violated. This is useful for the purpose of debugging the library.

Definition at line 881 of file Grid_public.cc.

Referenced by congruence_widening_assign(), construct(), generator_widening_assign(), Grid(), intersection_assign(), is_included_in(), map_space_dimensions(), simplify_using_context_assign(), time_elapse_assign(), and upper_bound_assign().

                                      {
#ifndef NDEBUG
  using std::endl;
  using std::cerr;
#endif

  // Check whether the status information is legal.
  if (!status.OK())
    goto fail;

  if (marked_empty()) {
    if (check_not_empty) {
      // The caller does not want the grid to be empty.
#ifndef NDEBUG
      cerr << "Empty grid!" << endl;
#endif
      goto fail;
    }

    if (con_sys.space_dimension() != space_dim) {
#ifndef NDEBUG
      cerr << "The grid is in a space of dimension " << space_dim
           << " while the system of congruences is in a space of dimension "
           << con_sys.space_dimension()
           << endl;
#endif
      goto fail;
    }
    return true;
  }

  // A zero-dimensional universe grid is legal only if the system of
  // congruences `con_sys' is empty, and the generator system contains
  // one point.
  if (space_dim == 0) {
    if (con_sys.has_no_rows())
      if (gen_sys.num_rows() == 1 && gen_sys[0].is_point())
        return true;
#ifndef NDEBUG
    cerr << "Zero-dimensional grid should have an empty congruence" << endl
         << "system and a generator system of a single point." << endl;
#endif
    goto fail;
  }

  // A grid is defined by a system of congruences or a system of
  // generators.  At least one of them must be up to date.
  if (!congruences_are_up_to_date() && !generators_are_up_to_date()) {
#ifndef NDEBUG
    cerr << "Grid not empty, not zero-dimensional" << endl
         << "and with neither congruences nor generators up-to-date!"
         << endl;
#endif
    goto fail;
  }

  {
    // The expected number of columns in the congruence and generator
    // systems, if they are not empty.
    const dimension_type num_columns = space_dim + 1;

    // Here we check if the size of the matrices is consistent.
    // Let us suppose that all the matrices are up-to-date; this means:
    // `con_sys' : number of congruences x poly_num_columns
    // `gen_sys' : number of generators  x poly_num_columns
    if (congruences_are_up_to_date())
      if (con_sys.num_columns() != num_columns + 1 /* moduli */) {
#ifndef NDEBUG
        cerr << "Incompatible size! (con_sys and space_dim)"
             << endl;
#endif
        goto fail;
      }

    if (generators_are_up_to_date()) {
      if (gen_sys.space_dimension() + 1 != num_columns) {
#ifndef NDEBUG
        cerr << "Incompatible size! (gen_sys and space_dim)"
             << endl;
#endif
        goto fail;
      }

      // Check if the system of generators is well-formed.
      if (!gen_sys.OK())
        goto fail;

      // Check each generator in the system.
      for (dimension_type i = gen_sys.num_rows(); i-- > 0; ) {
        const Grid_Generator& g = gen_sys[i];

        if (g.size() < 1) {
#ifndef NDEBUG
          cerr << "Parameter should have coefficients." << endl;
#endif
          goto fail;
        }
      }

      // A non-empty system of generators describing a grid is valid
      // if and only if it contains a point.
      if (!gen_sys.has_no_rows() && !gen_sys.has_points()) {
#ifndef NDEBUG
        cerr << "Non-empty generator system declared up-to-date "
             << "has no points!"
             << endl;
#endif
        goto fail;
      }

      if (generators_are_minimized()) {
        Grid_Generator_System gs = gen_sys;

        if (dim_kinds.size() != num_columns) {
#ifndef NDEBUG
          cerr << "Size of dim_kinds should equal the number of columns."
               << endl;
#endif
          goto fail;
        }

        if (!upper_triangular(gs, dim_kinds)) {
#ifndef NDEBUG
          cerr << "Reduced generators should be upper triangular."
               << endl;
#endif
          goto fail;
        }

        // Check that dim_kinds corresponds to the row kinds in gen_sys.
        for (dimension_type dim = space_dim,
               row = gen_sys.num_rows(); dim > 0; --dim) {
          if (dim_kinds[dim] == GEN_VIRTUAL)
            goto ok;
          if (gen_sys[--row].is_parameter_or_point()
              && dim_kinds[dim] == PARAMETER)
            goto ok;
          PPL_ASSERT(gen_sys[row].is_line());
          if (dim_kinds[dim] == LINE)
            goto ok;
#ifndef NDEBUG
          cerr << "Kinds in dim_kinds should match those in gen_sys."
               << endl;
#endif
          goto fail;
        ok:
          PPL_ASSERT(row <= dim);
        }

        // A reduced generator system must be the same as a temporary
        // reduced copy.
        Dimension_Kinds dim_kinds_copy = dim_kinds;
        // `gs' is minimized and marked_empty returned false, so `gs'
        // should contain rows.
        PPL_ASSERT(!gs.has_no_rows());
        simplify(gs, dim_kinds_copy);
        // gs contained rows before being reduced, so it should
        // contain at least a single point afterward.
        PPL_ASSERT(!gs.has_no_rows());
        for (dimension_type row = gen_sys.num_rows(); row-- > 0; ) {
          Grid_Generator& g = gs[row];
          const Grid_Generator& g_copy = gen_sys[row];
          if (g.is_equal_to(g_copy))
            continue;
#ifndef NDEBUG
          cerr << "Generators are declared minimized,"
            " but they change under reduction.\n"
               << "Here is the generator system:\n";
          gen_sys.ascii_dump(cerr);
          cerr << "and here is the minimized form of the temporary copy:\n";
          gs.ascii_dump(cerr);
#endif
          goto fail;
        }
      }

    } // if (congruences_are_up_to_date())
  }

  if (congruences_are_up_to_date()) {
    // Check if the system of congruences is well-formed.
    if (!con_sys.OK())
      goto fail;

    Grid tmp_gr = *this;
    // Make a copy here, before changing tmp_gr, to check later.
    const Congruence_System cs_copy = tmp_gr.con_sys;

    // Clear the generators in tmp_gr.
    Grid_Generator_System gs(space_dim);
    tmp_gr.gen_sys.m_swap(gs);
    tmp_gr.clear_generators_up_to_date();

    if (!tmp_gr.update_generators()) {
      if (check_not_empty) {
        // Want to know the satisfiability of the congruences.
#ifndef NDEBUG
        cerr << "Unsatisfiable system of congruences!"
             << endl;
#endif
        goto fail;
      }
      // The grid is empty, all checks are done.
      return true;
    }

    if (congruences_are_minimized()) {
      // A reduced congruence system must be lower triangular.
      if (!lower_triangular(con_sys, dim_kinds)) {
#ifndef NDEBUG
        cerr << "Reduced congruences should be lower triangular." << endl;
#endif
        goto fail;
      }

      // If the congruences are minimized, all the elements in the
      // congruence system must be the same as those in the temporary,
      // minimized system `cs_copy'.
      if (!con_sys.is_equal_to(cs_copy)) {
#ifndef NDEBUG
        cerr << "Congruences are declared minimized, but they change under reduction!"
             << endl
             << "Here is the minimized form of the congruence system:"
             << endl;
        cs_copy.ascii_dump(cerr);
        cerr << endl;
#endif
        goto fail;
      }

      if (dim_kinds.size() != con_sys.num_columns() - 1 /* modulus */) {
#ifndef NDEBUG
        cerr << "Size of dim_kinds should equal the number of columns."
             << endl;
#endif
        goto fail;
      }

      // Check that dim_kinds corresponds to the row kinds in con_sys.
      for (dimension_type dim = space_dim, row = 0; dim > 0; --dim) {
        if (dim_kinds[dim] == CON_VIRTUAL)
            continue;
        if (con_sys[row++].is_proper_congruence()
            && dim_kinds[dim] == PROPER_CONGRUENCE)
          continue;
        PPL_ASSERT(con_sys[row-1].is_equality());
        if (dim_kinds[dim] == EQUALITY)
          continue;
#ifndef NDEBUG
        cerr << "Kinds in dim_kinds should match those in con_sys." << endl;
#endif
        goto fail;
      }
    }
  }

  return true;

 fail:
#ifndef NDEBUG
  cerr << "Here is the grid under check:" << endl;
  ascii_dump(cerr);
#endif
  return false;
}

PPL::Grid & Parma_Polyhedra_Library::Grid::operator= ( const Grid & y )

The assignment operator. (*this and y can be dimension-incompatible.)

Definition at line 242 of file Grid_public.cc.

References con_sys, congruences_are_up_to_date(), dim_kinds, gen_sys, generators_are_up_to_date(), marked_empty(), space_dim, and status.

                                {
  space_dim = y.space_dim;
  dim_kinds = y.dim_kinds;
  if (y.marked_empty())
    set_empty();
  else if (space_dim == 0)
    set_zero_dim_univ();
  else {
    status = y.status;
    if (y.congruences_are_up_to_date())
      con_sys = y.con_sys;
    if (y.generators_are_up_to_date())
      gen_sys = y.gen_sys;
  }
  return *this;
}

void Parma_Polyhedra_Library::Grid::print ( ) const

Prints *this to std::cerr using operator<<.

PPL::Grid::Three_Valued_Boolean Parma_Polyhedra_Library::Grid::quick_equivalence_test ( const Grid & y ) const

private

Polynomial but incomplete equivalence test between grids.

Definition at line 181 of file Grid_nonpublic.cc.

References con_sys, congruences_are_minimized(), gen_sys, generators_are_minimized(), marked_empty(), Parma_Polyhedra_Library::Congruence_System::num_equalities(), Parma_Polyhedra_Library::Grid_Generator_System::num_lines(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), Parma_Polyhedra_Library::Grid_Generator_System::num_rows(), PPL_ASSERT, space_dim, TVB_DONT_KNOW, TVB_FALSE, and TVB_TRUE.

Referenced by contains(), and operator==().

                                                   {
  // Private method: the caller must ensure the following.
  PPL_ASSERT(space_dim == y.space_dim);
  PPL_ASSERT(!marked_empty() && !y.marked_empty() && space_dim > 0);

  const Grid& x = *this;

  bool css_normalized = false;

  if (x.congruences_are_minimized() && y.congruences_are_minimized()) {
    // Equivalent minimized congruence systems have:
    //  - the same number of congruences; ...
    if (x.con_sys.num_rows() != y.con_sys.num_rows())
      return Grid::TVB_FALSE;
    //  - the same number of equalities; ...
    dimension_type x_num_equalities = x.con_sys.num_equalities();
    if (x_num_equalities != y.con_sys.num_equalities())
      return Grid::TVB_FALSE;
    //  - and if there are no equalities, the same congruences.
    //    Delay this test: try cheaper tests on generators first.
    css_normalized = (x_num_equalities == 0);
  }

  if (x.generators_are_minimized() && y.generators_are_minimized()) {
    // Equivalent minimized generator systems have:
    //  - the same number of generators; ...
    if (x.gen_sys.num_rows() != y.gen_sys.num_rows())
      return Grid::TVB_FALSE;
    //  - the same number of lines; ...
    const dimension_type x_num_lines = x.gen_sys.num_lines();
    if (x_num_lines != y.gen_sys.num_lines())
      return Grid::TVB_FALSE;
      //  - and if there are no lines, the same generators.
    if (x_num_lines == 0) {
      // Check for syntactic identity.
      if (x.gen_sys == y.gen_sys)
        return Grid::TVB_TRUE;
      else
        return Grid::TVB_FALSE;
    }
  }

  // TODO: Consider minimizing the systems and re-performing these
  //       checks.

  if (css_normalized) {
    if (x.con_sys == y.con_sys)
      return Grid::TVB_TRUE;
    else
      return Grid::TVB_FALSE;
  }

  return Grid::TVB_DONT_KNOW;
}

void Parma_Polyhedra_Library::Grid::reduce_congruence_with_equality	(	Congruence &	row,
		const Congruence &	pivot,
		dimension_type	column,
		Congruence_System &	sys
	)

staticprivate

Reduce row using pivot.

Use the equality pivot to change the representation of the congruence row such that element at index column of row is zero.

Definition at line 181 of file Grid_simplify.cc.

References Parma_Polyhedra_Library::exact_div_assign(), Parma_Polyhedra_Library::gcd_assign(), Parma_Polyhedra_Library::Congruence::is_proper_congruence(), Parma_Polyhedra_Library::Congruence::modulus(), Parma_Polyhedra_Library::neg_assign(), Parma_Polyhedra_Library::Dense_Matrix::num_columns(), Parma_Polyhedra_Library::Dense_Matrix::num_rows(), PPL_ASSERT, PPL_DIRTY_TEMP_COEFFICIENT, and Parma_Polyhedra_Library::sub_mul_assign().

Referenced by simplify().

                                                              {
  // Very similar to reduce_parameter_with_line above.  Any change
  // here may be needed there too.
  PPL_ASSERT(row.modulus() > 0 && pivot.modulus() == 0);

  const Coefficient& pivot_column = pivot[column];
  Coefficient& row_column = row[column];

  dimension_type num_columns = sys.num_columns();

  // If the elements at `column' in row and pivot are the same, then
  // just subtract `pivot' from `row'.
  if (row_column == pivot_column) {
    for (dimension_type col = num_columns; col-- > 0; )
      row[col] -= pivot[col];
    return;
  }

  PPL_DIRTY_TEMP_COEFFICIENT(reduced_row_col);
  // Use reduced_row_col temporarily to hold the gcd.
  gcd_assign(reduced_row_col, pivot_column, row_column);
  PPL_DIRTY_TEMP_COEFFICIENT(reduced_pivot_col);
  exact_div_assign(reduced_pivot_col, pivot_column, reduced_row_col);
  exact_div_assign(reduced_row_col, row_column, reduced_row_col);
  // Ensure that `reduced_pivot_col' is positive, so that the modulus
  // remains positive when multiplying the proper congruences below.
  // It's safe to swap the signs as row[column] will still come out 0.
  if (reduced_pivot_col < 0) {
    neg_assign(reduced_pivot_col);
    neg_assign(reduced_row_col);
  }
  // Multiply `row', including the modulus, by reduced_pivot_col.  To
  // keep all the moduli the same this requires multiplying all the
  // other proper congruences in the same way.
  for (dimension_type index = sys.num_rows(); index-- > 0; ) {
    Congruence& cg = sys[index];
    if (cg.is_proper_congruence())
      for (dimension_type col = num_columns; col-- > 0; )
        cg[col] *= reduced_pivot_col;
  }
  // Column num_columns contains the modulus, so start at the next
  // column.
  --num_columns;
  row_column = 0;
  // Subtract from row a multiple of pivot such that the result in
  // row[column] is zero.
  for (dimension_type col = column; col-- > 0; )
    sub_mul_assign(row[col], reduced_row_col, pivot[col]);
}

void Parma_Polyhedra_Library::Grid::reduce_equality_with_equality	(	Congruence &	row,
		const Congruence &	pivot,
		dimension_type	column
	)

staticprivate

Reduces the equality row using the equality pivot.

Uses the equality pivot to change the representation of the equality row so that the element at index column of row is zero.

Definition at line 57 of file Grid_simplify.cc.

References Parma_Polyhedra_Library::exact_div_assign(), Parma_Polyhedra_Library::gcd_assign(), Parma_Polyhedra_Library::Congruence::modulus(), PPL_ASSERT, PPL_DIRTY_TEMP_COEFFICIENT, and Parma_Polyhedra_Library::sub_mul_assign().

Referenced by simplify().

                                                                 {
  // Assume two equalities.
  PPL_ASSERT(row.modulus() == 0 && pivot.modulus() == 0);

  const Coefficient& pivot_column = pivot[column];
  Coefficient& row_column = row[column];
  PPL_DIRTY_TEMP_COEFFICIENT(reduced_row_col);
  // Use reduced_row_col temporarily to hold the gcd.
  gcd_assign(reduced_row_col, pivot_column, row_column);
  // Store the reduced ratio between pivot[column] and row[column].
  PPL_DIRTY_TEMP_COEFFICIENT(reduced_pivot_col);
  exact_div_assign(reduced_pivot_col, pivot_column, reduced_row_col);
  exact_div_assign(reduced_row_col, row_column, reduced_row_col);
  // Multiply row, then subtract from it a multiple of pivot such that
  // the result in row[column] is zero.
  row_column = 0;
  for (dimension_type col = column; col-- > 0; ) {
    Coefficient& row_col = row[col];
    row_col *= reduced_pivot_col;
    sub_mul_assign(row_col, reduced_row_col, pivot[col]);
  }
}

void Parma_Polyhedra_Library::Grid::reduce_line_with_line	(	Grid_Generator &	row,
		Grid_Generator &	pivot,
		dimension_type	column
	)

staticprivate

Reduces the line row using the line pivot.

Uses the line pivot to change the representation of the line row so that the element at index column of row is zero.

Definition at line 31 of file Grid_simplify.cc.

References Parma_Polyhedra_Library::exact_div_assign(), Parma_Polyhedra_Library::gcd_assign(), PPL_DIRTY_TEMP_COEFFICIENT, Parma_Polyhedra_Library::Grid_Generator::size(), and Parma_Polyhedra_Library::sub_mul_assign().

Referenced by simplify().

                                                   {
  const Coefficient& pivot_column = pivot[column];
  Coefficient& row_column = row[column];
  PPL_DIRTY_TEMP_COEFFICIENT(reduced_row_col);
  // Use reduced_row_col temporarily to hold the gcd.
  gcd_assign(reduced_row_col, pivot_column, row_column);
  // Store the reduced ratio between pivot[column] and row[column].
  PPL_DIRTY_TEMP_COEFFICIENT(reduced_pivot_col);
  exact_div_assign(reduced_pivot_col, pivot_column, reduced_row_col);
  exact_div_assign(reduced_row_col, row_column, reduced_row_col);
  // Multiply row, then subtract from it a multiple of pivot such that
  // the result in row[column] is zero.
  row_column = 0;
  // pivot.size() - 1 is the index for the parameter divisor so we
  // start reducing the line at index pivot.size() - 2.
  for (dimension_type col = pivot.size() - 2;
       col > column;
       --col) {
    Coefficient& row_col = row[col];
    row_col *= reduced_pivot_col;
    sub_mul_assign(row_col, reduced_row_col, pivot[col]);
  }
}

void Parma_Polyhedra_Library::Grid::reduce_parameter_with_line	(	Grid_Generator &	row,
		const Grid_Generator &	pivot,
		dimension_type	column,
		Grid_Generator_System &	sys
	)

staticprivate

Reduce row using pivot.

Use the line pivot to change the representation of the parameter row such that the element at index column of row is zero.

Definition at line 125 of file Grid_simplify.cc.

References Parma_Polyhedra_Library::exact_div_assign(), Parma_Polyhedra_Library::gcd_assign(), Parma_Polyhedra_Library::Grid_Generator::is_parameter_or_point(), Parma_Polyhedra_Library::neg_assign(), Parma_Polyhedra_Library::Grid_Generator_System::num_columns(), Parma_Polyhedra_Library::Grid_Generator_System::num_rows(), PPL_DIRTY_TEMP_COEFFICIENT, and Parma_Polyhedra_Library::sub_mul_assign().

Referenced by simplify().

                                                             {
  // Very similar to reduce_congruence_with_equality below.  Any
  // change here may be needed there too.

  const Coefficient& pivot_column = pivot[column];
  Coefficient& row_column = row[column];

  // Subtract one to allow for the parameter divisor column
  const dimension_type num_columns = sys.num_columns() - 1;

  // If the elements at column in row and pivot are the same, then
  // just subtract pivot from row.
  if (row_column == pivot_column) {
    for (dimension_type col = num_columns; col-- > 0; )
      row[col] -= pivot[col];
    return;
  }

  PPL_DIRTY_TEMP_COEFFICIENT(reduced_row_col);
  // Use reduced_row_col temporarily to hold the gcd.
  gcd_assign(reduced_row_col, pivot_column, row_column);
  // Store the reduced ratio between pivot[column] and row[column].
  PPL_DIRTY_TEMP_COEFFICIENT(reduced_pivot_col);
  exact_div_assign(reduced_pivot_col, pivot_column, reduced_row_col);
  exact_div_assign(reduced_row_col, row_column, reduced_row_col);


  // Since we are reducing the system to "strong minimal form",
  // ensure that the multiplier is positive, so that the preceding
  // diagonals (including the divisor) remain positive.  It's safe to
  // swap the signs as row[column] will still come out 0.
  if (reduced_pivot_col < 0) {
    neg_assign(reduced_pivot_col);
    neg_assign(reduced_row_col);
  }

  // Multiply row such that a multiple of pivot can be subtracted from
  // it below to render row[column] zero.  This requires multiplying
  // all other parameters to match.
  for (dimension_type index = sys.num_rows(); index-- > 0; ) {
    Grid_Generator& gen = sys[index];
    if (gen.is_parameter_or_point())
      for (dimension_type col = num_columns; col-- > 0; )
        gen[col] *= reduced_pivot_col;
  }
  // Subtract from row a multiple of pivot such that the result in
  // row[column] is zero.
  row_column = 0;
  for (dimension_type col = num_columns - 1; col > column; --col)
    sub_mul_assign(row[col], reduced_row_col, pivot[col]);
}

template<typename R >

void Parma_Polyhedra_Library::Grid::reduce_pc_with_pc	(	R &	row,
		R &	pivot,
		dimension_type	column,
		dimension_type	start,
		dimension_type	end
	)

staticprivate

Reduces row using pivot.

Uses the point, parameter or proper congruence at pivot to change the representation of the point, parameter or proper congruence at row so that the element at index column of row is zero. Only elements from index start to index end are modified (i.e. it is assumed that all other elements are zero).

Definition at line 84 of file Grid_simplify.cc.

References Parma_Polyhedra_Library::add_mul_assign(), Parma_Polyhedra_Library::exact_div_assign(), Parma_Polyhedra_Library::gcdext_assign(), PPL_ASSERT, PPL_DIRTY_TEMP_COEFFICIENT, and Parma_Polyhedra_Library::sub_mul_assign().

Referenced by simplify().

                                                  {
  Coefficient& pivot_column = pivot[column];
  Coefficient& row_column = row[column];

  PPL_DIRTY_TEMP_COEFFICIENT(s);
  PPL_DIRTY_TEMP_COEFFICIENT(t);
  PPL_DIRTY_TEMP_COEFFICIENT(reduced_row_col);
  // Use reduced_row_col temporarily to hold the gcd.
  gcdext_assign(reduced_row_col, s, t, pivot_column, row_column);
  // Now pivot[column] * s + row[column] * t == gcd.

  // Store the reduced ratio between pivot[column] and row[column].
  PPL_DIRTY_TEMP_COEFFICIENT(reduced_pivot_col);
  exact_div_assign(reduced_pivot_col, pivot_column, reduced_row_col);
  pivot_column = reduced_row_col /* gcd */;
  exact_div_assign(reduced_row_col, row_column, reduced_row_col);

  // Multiply row, then subtract from it a multiple of pivot such that
  // the result in row[column] is zero.  Afterward, multiply pivot,
  // then add to it a (possibly negative) multiple of row such that
  // the result in pivot[column] is the smallest possible positive
  // integer.
  PPL_ASSERT(pivot.size() > 0);
  PPL_ASSERT(row.size() > 0);
  row_column = 0;
  PPL_DIRTY_TEMP_COEFFICIENT(old_pivot_col);
  for (dimension_type col = start; col < end; ++col) {
    Coefficient& pivot_col = pivot[col];
    old_pivot_col = pivot_col;
    pivot_col *= s;
    Coefficient& row_col = row[col];
    add_mul_assign(pivot_col, t, row_col);
    row_col *= reduced_pivot_col;
    sub_mul_assign(row_col, reduced_row_col, old_pivot_col);
  }
}

template<typename M , typename R >

void Parma_Polyhedra_Library::Grid::reduce_reduced	(	M &	sys,
		dimension_type	dim,
		dimension_type	pivot_index,
		dimension_type	start,
		dimension_type	end,
		const Dimension_Kinds &	sys_dim_kinds,
		bool	generators = `true`
	)

staticprivate

Reduce column dim in rows preceding pivot_index in sys.

Required when converting (or simplifying) a congruence or generator system to "strong minimal form"; informally, strong minimal form means that, not only is the system in minimal form (ie a triangular matrix), but also the absolute values of the coefficients of the proper congruences and parameters are minimal. As a simple example, the set of congruences $\{3x \equiv_3 0, 4x + y \equiv_3 1\}$ , (which is in minimal form) is equivalent to the set $\{3x \equiv_3 0, x + y \equiv_3 1\}$ (which is in strong minimal form).

Parameters:

sys	The generator or congruence system to be reduced to strong minimal form.
dim	Column to be reduced.
pivot_index	Index of last row to be reduced.
start	Index of first column to be changed.
end	Index of last column to be changed.
sys_dim_kinds	Dimension kinds of the elements of `sys`.
generators	Flag indicating whether `sys` is a congruence or generator system

Definition at line 268 of file Grid.templates.hh.

References CON_VIRTUAL, EQUALITY, GEN_VIRTUAL, LINE, PARAMETER, PPL_DIRTY_TEMP_COEFFICIENT, row_index, and Parma_Polyhedra_Library::sub_mul_assign().

                                            {
  R& pivot = sys[pivot_index];

  const Coefficient& pivot_dim = pivot[dim];

  if (pivot_dim == 0)
    return;

  PPL_DIRTY_TEMP_COEFFICIENT(pivot_dim_half);
  pivot_dim_half = (pivot_dim + 1) / 2;
  const Dimension_Kind row_kind = sys_dim_kinds[dim];
  const bool row_is_line_or_equality
    = (row_kind == (generators ? LINE : EQUALITY));

  PPL_DIRTY_TEMP_COEFFICIENT(num_rows_to_subtract);
  PPL_DIRTY_TEMP_COEFFICIENT(row_dim_remainder);
  for (dimension_type kinds_index = dim,
         row_index = pivot_index; row_index-- > 0; ) {
    if (generators) {
      --kinds_index;
      // Move over any virtual rows.
      while (sys_dim_kinds[kinds_index] == GEN_VIRTUAL)
        --kinds_index;
    }
    else {
      ++kinds_index;
      // Move over any virtual rows.
      while (sys_dim_kinds[kinds_index] == CON_VIRTUAL)
        ++kinds_index;
    }

    // row_kind CONGRUENCE is included as PARAMETER
    if (row_is_line_or_equality
        || (row_kind == PARAMETER
            && sys_dim_kinds[kinds_index] == PARAMETER)) {
      R& row = sys[row_index];

      const Coefficient& row_dim = row[dim];
      // num_rows_to_subtract may be positive or negative.
      num_rows_to_subtract = row_dim / pivot_dim;

      // Ensure that after subtracting num_rows_to_subtract * r_dim
      // from row_dim, -pivot_dim_half < row_dim <= pivot_dim_half.
      // E.g., if pivot[dim] = 9, then after this reduction
      // -5 < row_dim <= 5.
      row_dim_remainder = row_dim % pivot_dim;
      if (row_dim_remainder < 0) {
        if (row_dim_remainder <= -pivot_dim_half)
          --num_rows_to_subtract;
      }
      else if (row_dim_remainder > 0 && row_dim_remainder > pivot_dim_half)
        ++num_rows_to_subtract;

      // Subtract num_rows_to_subtract copies of pivot from row i.  Only the
      // entries from dim need to be subtracted, as the preceding
      // entries are all zero.
      // If num_rows_to_subtract is negative, these copies of pivot are
      // added to row i.
      if (num_rows_to_subtract != 0)
        for (dimension_type col = start; col <= end; ++col)
          sub_mul_assign(row[col], num_rows_to_subtract, pivot[col]);
    }
  }
}

void Parma_Polyhedra_Library::Grid::refine_no_check ( const Constraint & c )

private

Uses the constraint c to refine *this.

Parameters:

c	The constraint to be added. Non-trivial inequalities are ignored.

Warning:: If c and *this are dimension-incompatible, the behavior is undefined.

Definition at line 694 of file Grid_nonpublic.cc.

References Parma_Polyhedra_Library::Constraint::is_equality(), Parma_Polyhedra_Library::Constraint::is_inconsistent(), PPL_ASSERT, and Parma_Polyhedra_Library::Constraint::space_dimension().

                                            {
  PPL_ASSERT(!marked_empty());
  PPL_ASSERT(space_dim >= c.space_dimension());

  if (c.is_equality()) {
    Congruence cg(c);
    add_congruence_no_check(cg);
  }
  else if (c.is_inconsistent())
    set_empty();
}

void Parma_Polyhedra_Library::Grid::refine_with_congruence ( const Congruence & cg )

inline

Uses a copy of the congruence cg to refine *this.

Parameters:

cg	The congruence used.

Exceptions:

std::invalid_argument Thrown if *this and congruence cg are dimension-incompatible.

Definition at line 282 of file Grid.inlines.hh.

References add_congruence().

Referenced by Parma_Polyhedra_Library::Affine_Space::refine_with_congruence().

                                                 {
  add_congruence(cg);
}

void Parma_Polyhedra_Library::Grid::refine_with_congruences ( const Congruence_System & cgs )

inline

Uses a copy of the congruences in cgs to refine *this.

Parameters:

cgs	The congruences used.

Exceptions:

std::invalid_argument Thrown if *this and cgs are dimension-incompatible.

Definition at line 287 of file Grid.inlines.hh.

References add_congruences().

Referenced by Parma_Polyhedra_Library::Affine_Space::refine_with_congruences().

                                                          {
  add_congruences(cgs);
}

void Parma_Polyhedra_Library::Grid::refine_with_constraint ( const Constraint & c )

Uses a copy of the constraint c to refine *this.

Parameters:

c	The constraint used. If it is not an equality, it will be ignored

Exceptions:

std::invalid_argument Thrown if *this and c are dimension-incompatible.

Definition at line 1315 of file Grid_public.cc.

References Parma_Polyhedra_Library::Constraint::space_dimension().

                                                   {
  // The dimension of `c' must be at most `space_dim'.
  if (space_dim < c.space_dimension())
    throw_dimension_incompatible("refine_with_constraint(c)", "c", c);
  if (marked_empty())
    return;
  refine_no_check(c);
}

void Parma_Polyhedra_Library::Grid::refine_with_constraints ( const Constraint_System & cs )

Uses a copy of the constraints in cs to refine *this.

Parameters:

cs	The constraints used. Constraints that are not equalities are ignored.

Exceptions:

std::invalid_argument Thrown if *this and cs are dimension-incompatible.

Definition at line 1325 of file Grid_public.cc.

References Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Constraint_System::end(), and Parma_Polyhedra_Library::Constraint_System::space_dimension().

                                                            {
  // The dimension of `cs' must be at most `space_dim'.
  if (space_dim < cs.space_dimension())
    throw_dimension_incompatible("refine_with_constraints(cs)", "cs", cs);

  for (Constraint_System::const_iterator i = cs.begin(),
         cs_end = cs.end(); !marked_empty() && i != cs_end; ++i)
    refine_no_check(*i);
}

PPL::Poly_Con_Relation Parma_Polyhedra_Library::Grid::relation_with ( const Congruence & cg ) const

Returns the relations holding between *this and cg.

Definition at line 363 of file Grid_public.cc.

Referenced by difference_assign(), limited_congruence_extrapolation_assign(), limited_extrapolation_assign(), limited_generator_extrapolation_assign(), and simplify_using_context_assign().

                                                 {
  // Dimension-compatibility check.
  if (space_dim < cg.space_dimension())
    throw_dimension_incompatible("relation_with(cg)", "cg", cg);

  if (marked_empty())
    return Poly_Con_Relation::saturates()
      && Poly_Con_Relation::is_included()
      && Poly_Con_Relation::is_disjoint();

  if (space_dim == 0) {
    if (cg.is_inconsistent())
      return Poly_Con_Relation::is_disjoint();
    else if (cg.is_equality())
      return Poly_Con_Relation::saturates()
        && Poly_Con_Relation::is_included();
    else if (cg.inhomogeneous_term() % cg.modulus() == 0)
      return Poly_Con_Relation::saturates()
        && Poly_Con_Relation::is_included();
  }

  if (!generators_are_up_to_date() && !update_generators())
    // Updating found the grid empty.
    return Poly_Con_Relation::saturates()
      && Poly_Con_Relation::is_included()
      && Poly_Con_Relation::is_disjoint();

  // Return one of the relations
  // 'strictly_intersects'   a strict subset of the grid points satisfy cg
  // 'is_included'           every grid point satisfies cg
  // 'is_disjoint'           cg and the grid occupy separate spaces.

  // There is always a point.

  // Scalar product of the congruence and the first point that
  // satisfies the congruence.
  PPL_DIRTY_TEMP_COEFFICIENT(point_sp);
  point_sp = 0;

  PPL_DIRTY_TEMP_COEFFICIENT(div);
  div = cg.modulus();

  PPL_DIRTY_TEMP_COEFFICIENT(sp);

  bool known_to_intersect = false;

  for (Grid_Generator_System::const_iterator i = gen_sys.begin(),
         i_end = gen_sys.end(); i != i_end; ++i) {
    const Grid_Generator& g = *i;
    Scalar_Products::assign(sp, cg, g);

    switch (g.type()) {

    case Grid_Generator::POINT:
      if (cg.is_proper_congruence())
        sp %= div;
      if (sp == 0) {
        // The point satisfies the congruence.
        if (point_sp == 0)
          // Any previous points satisfied the congruence.
          known_to_intersect = true;
        else
          return Poly_Con_Relation::strictly_intersects();
      }
      else {
        if (point_sp == 0) {
          if (known_to_intersect)
            return Poly_Con_Relation::strictly_intersects();
          // Assign `sp' to `point_sp' as `sp' is the scalar product
          // of cg and a point g and is non-zero.
          point_sp = sp;
        }
        else {
          // A previously considered point p failed to satisfy cg such that
          // `point_sp' = `scalar_prod(p, cg)'
          // so, if we consider the parameter g-p instead of g, we have
          // scalar_prod(g-p, cg) = scalar_prod(g, cg) - scalar_prod(p, cg)
          //                      = sp - point_sp
          sp -= point_sp;

          if (sp != 0) {
            // Find the GCD between sp and the previous GCD.
            gcd_assign(div, div, sp);
            if (point_sp % div == 0)
              // There is a point in the grid satisfying cg.
              return Poly_Con_Relation::strictly_intersects();
          }
        }
      }
      break;

    case Grid_Generator::PARAMETER:
      if (cg.is_proper_congruence())
        sp %= (div * g.divisor());
      if (sp == 0)
        // Parameter g satisfies the cg so the relation depends
        // entirely on the other generators.
        break;
      if (known_to_intersect)
        // At least one point satisfies cg.  However, the sum of such
        // a point and the parameter g fails to satisfy cg (due to g).
        return Poly_Con_Relation::strictly_intersects();
      // Find the GCD between sp and the previous GCD.
      gcd_assign(div, div, sp);
      if (point_sp != 0) {
        // At least one of any previously encountered points fails to
        // satisfy cg.
        if (point_sp % div == 0)
          // There is also a grid point that satisfies cg.
          return Poly_Con_Relation::strictly_intersects();
      }
      break;

    case Grid_Generator::LINE:
      if (sp == 0)
        // Line g satisfies the cg so the relation depends entirely on
        // the other generators.
        break;

      // Line g intersects the congruence.
      //
      // There is a point p in the grid.  Suppose <p*cg> = p_sp.  Then
      // (-p_sp/sp)*g + p is a point that satisfies cg: <((-p_sp/sp)*g
      // + p).cg> = -(p_sp/sp)*sp + p_sp) = 0.  If p does not satisfy
      // `cg' and hence is not in the grid defined by `cg', the grid
      // `*this' strictly intersects the `cg' grid.  On the other
      // hand, if `p' is in the grid defined by `cg' so that p_sp = 0,
      // then <p+g.cg> = p_sp + sp != 0; thus `p+g' is a point in
      // *this that does not satisfy `cg' and hence `p+g' is a point
      // in *this not in the grid defined by `cg'; therefore `*this'
      // strictly intersects the `cg' grid.
      return Poly_Con_Relation::strictly_intersects();
    }
  }

  if (point_sp == 0) {
    if (cg.is_equality())
      // Every generator satisfied the cg.
      return Poly_Con_Relation::is_included()
        && Poly_Con_Relation::saturates();
    else
      // Every generator satisfied the cg.
      return Poly_Con_Relation::is_included();
  }

  PPL_ASSERT(!known_to_intersect);
  return Poly_Con_Relation::is_disjoint();
}

PPL::Poly_Gen_Relation Parma_Polyhedra_Library::Grid::relation_with ( const Grid_Generator & g ) const

Returns the relations holding between *this and g.

Definition at line 513 of file Grid_public.cc.

References Parma_Polyhedra_Library::Poly_Gen_Relation::nothing(), Parma_Polyhedra_Library::Grid_Generator::space_dimension(), and Parma_Polyhedra_Library::Poly_Gen_Relation::subsumes().

                                                    {
  // Dimension-compatibility check.
  if (space_dim < g.space_dimension())
    throw_dimension_incompatible("relation_with(g)", "g", g);

  // The empty grid cannot subsume a generator.
  if (marked_empty())
    return Poly_Gen_Relation::nothing();

  // A universe grid in a zero-dimensional space subsumes all the
  // generators of a zero-dimensional space.
  if (space_dim == 0)
    return Poly_Gen_Relation::subsumes();

  if (!congruences_are_up_to_date())
    update_congruences();

  return
    con_sys.satisfies_all_congruences(g)
    ? Poly_Gen_Relation::subsumes()
    : Poly_Gen_Relation::nothing();
}

PPL::Poly_Gen_Relation Parma_Polyhedra_Library::Grid::relation_with ( const Generator & g ) const

Returns the relations holding between *this and g.

Definition at line 537 of file Grid_public.cc.

References Parma_Polyhedra_Library::Generator::coefficient(), Parma_Polyhedra_Library::Generator::divisor(), Parma_Polyhedra_Library::Generator::is_closure_point(), Parma_Polyhedra_Library::Generator::is_point(), Parma_Polyhedra_Library::Poly_Gen_Relation::nothing(), Parma_Polyhedra_Library::Generator::space_dimension(), and Parma_Polyhedra_Library::Poly_Gen_Relation::subsumes().

                                               {
  dimension_type g_space_dim = g.space_dimension();

  // Dimension-compatibility check.
  if (space_dim < g_space_dim)
    throw_dimension_incompatible("relation_with(g)", "g", g);

  // The empty grid cannot subsume a generator.
  if (marked_empty())
    return Poly_Gen_Relation::nothing();

  // A universe grid in a zero-dimensional space subsumes all the
  // generators of a zero-dimensional space.
  if (space_dim == 0)
    return Poly_Gen_Relation::subsumes();

  if (!congruences_are_up_to_date())
    update_congruences();

  Linear_Expression expr;
  for (dimension_type i = g_space_dim; i-- > 0; ) {
    const Variable v(i);
    expr += g.coefficient(v) * v;
  }
  Grid_Generator gg(grid_point());
  if (g.is_point() || g.is_closure_point())
    // Points and closure points are converted to grid points.
    gg = grid_point(expr, g.divisor());
  else
    // The generator is a ray or line.
    // In both cases, we convert it to a grid line
    gg = grid_line(expr);

  return
    con_sys.satisfies_all_congruences(gg)
    ? Poly_Gen_Relation::subsumes()
    : Poly_Gen_Relation::nothing();
}

PPL::Poly_Con_Relation Parma_Polyhedra_Library::Grid::relation_with ( const Constraint & c ) const

Returns the relations holding between *this and c.

Definition at line 577 of file Grid_public.cc.

                                                {
  // Dimension-compatibility check.
  if (space_dim < c.space_dimension())
    throw_dimension_incompatible("relation_with(c)", "c", c);

  if (c.is_equality()) {
    Congruence cg(c);
    return relation_with(cg);
  }

  if (marked_empty())
    return Poly_Con_Relation::saturates()
      &&  Poly_Con_Relation::is_included()
      && Poly_Con_Relation::is_disjoint();

  if (space_dim == 0) {
    if (c.is_inconsistent())
      if (c.is_strict_inequality() && c.inhomogeneous_term() == 0)
        // The constraint 0 > 0 implicitly defines the hyperplane 0 = 0;
        // thus, the zero-dimensional point also saturates it.
        return Poly_Con_Relation::saturates()
          && Poly_Con_Relation::is_disjoint();
      else
        return Poly_Con_Relation::is_disjoint();
    else if (c.inhomogeneous_term() == 0)
      return Poly_Con_Relation::saturates()
        && Poly_Con_Relation::is_included();
    else
      // The zero-dimensional point saturates
      // neither the positivity constraint 1 >= 0,
      // nor the strict positivity constraint 1 > 0.
      return Poly_Con_Relation::is_included();
  }

  if (!generators_are_up_to_date() && !update_generators())
    // Updating found the grid empty.
    return Poly_Con_Relation::saturates()
      && Poly_Con_Relation::is_included()
      && Poly_Con_Relation::is_disjoint();

  // Return one of the relations
  // 'strictly_intersects'   a strict subset of the grid points satisfy c
  // 'is_included'           every grid point satisfies c
  // 'is_disjoint'           c and the grid occupy separate spaces.

  // There is always a point.

  bool point_is_included = false;
  bool point_saturates = false;
  const Grid_Generator* first_point = 0;

  for (Grid_Generator_System::const_iterator i = gen_sys.begin(),
         i_end = gen_sys.end(); i != i_end; ++i) {
    const Grid_Generator& g = *i;
    switch (g.type()) {
    case Grid_Generator::POINT:
      {
        if (first_point == 0) {
          first_point = &g;
          const int sign = Scalar_Products::sign(c, g);
          if (sign == 0)
            point_saturates = !c.is_strict_inequality();
          else if (sign > 0)
            point_is_included = !c.is_equality();
          break;
        }
        // Not the first point: convert `g' to be a parameter
        // and fall through into the parameter case.
        Grid_Generator& gen = const_cast<Grid_Generator&>(g);
        const Grid_Generator& point = *first_point;
        const Coefficient& p_div = g[0];
        if (p_div != Coefficient_one()) {
          for (dimension_type j = gen.size() - 1; j-- > 1; )
            gen[j] *= p_div;
        }
        const Coefficient& g_div = gen[0];
        if (g_div == Coefficient_one()) {
          for (dimension_type j = gen.size() - 1; j-- > 1; )
            gen[j] -= point[j];
        }
        else {
          for (dimension_type j = gen.size() - 1; j-- > 1; )
            sub_mul_assign(gen[j], g_div, point[j]);
        }
        gen[0] *= p_div;
        gen.strong_normalize();
        gen.set_is_parameter();
        PPL_ASSERT(gen.OK());
      }
      // Intentionally fall through.

    case Grid_Generator::PARAMETER:
    case Grid_Generator::LINE:
      {
        const int sign = c.is_strict_inequality()
          ? Scalar_Products::reduced_sign(c, g)
          : Scalar_Products::sign(c, g);
        if (sign != 0)
          return Poly_Con_Relation::strictly_intersects();
      }
      break;
    } // switch
  }

  // If this program point is reached, then all lines and parameters
  // saturate the constraint. Hence, the result is determined by
  // the previosly computed relation with the point.
  if (point_saturates)
    return Poly_Con_Relation::saturates()
      && Poly_Con_Relation::is_included();

  if (point_is_included)
    return Poly_Con_Relation::is_included();

  return Poly_Con_Relation::is_disjoint();
}

void Parma_Polyhedra_Library::Grid::remove_higher_space_dimensions ( dimension_type new_dimension )

Removes the higher dimensions of the vector space so that the resulting space will have dimension new_dimension..

Exceptions:

std::invalid_argument Thrown if new_dimensions is greater than the space dimension of *this.

Definition at line 309 of file Grid_chdims.cc.

References Parma_Polyhedra_Library::Congruence_System::increase_space_dimension(), PPL_ASSERT, Parma_Polyhedra_Library::swap(), and Parma_Polyhedra_Library::Congruence::zero_dim_false().

                                                                          {
  // Dimension-compatibility check.
  if (new_dimension > space_dim)
    throw_dimension_incompatible("remove_higher_space_dimensions(nd)",
                                 new_dimension);

  // The removal of no dimensions from any grid is a no-op.
  // Note that this case also captures the only legal removal of
  // dimensions from a grid in a 0-dim space.
  if (new_dimension == space_dim) {
    PPL_ASSERT(OK());
    return;
  }

  if (is_empty()) {
    // Removing dimensions from the empty grid just updates the space
    // dimension.
    space_dim = new_dimension;
    set_empty();
    PPL_ASSERT(OK());
    return;
  }

  if (new_dimension == 0) {
    // Removing all dimensions from a non-empty grid just returns the
    // zero-dimensional universe grid.
    set_zero_dim_univ();
    return;
  }

  // Favor the generators, as is done by is_empty().
  if (generators_are_up_to_date()) {
    gen_sys.remove_higher_space_dimensions(new_dimension);
    if (generators_are_minimized()) {
      // Count the actual number of rows that are now redundant.
      dimension_type num_redundant = 0;
      const dimension_type num_old_gs = space_dim - new_dimension;
      for (dimension_type row = 0; row < num_old_gs; ++row)
        if (dim_kinds[row] != GEN_VIRTUAL)
          ++num_redundant;
      if (num_redundant > 0) {
        // Chop zero rows from end of system, to keep minimal form.
        gen_sys.remove_trailing_rows(num_redundant);
        gen_sys.unset_pending_rows();
      }
      dim_kinds.resize(new_dimension + 1);
      // TODO: Consider if it is worth also preserving the congruences
      //       if they are also in minimal form.
    }
    clear_congruences_up_to_date();
    // Extend the zero dim false congruence system to the appropriate
    // dimension and then swap it with `con_sys'.
    Congruence_System cgs(Congruence::zero_dim_false());
    // Extra 2 columns for inhomogeneous term and modulus.
    cgs.increase_space_dimension(new_dimension + 2);
    con_sys.m_swap(cgs);
  }
  else {
    PPL_ASSERT(congruences_are_minimized());
    con_sys.remove_higher_space_dimensions(new_dimension);
    // Count the actual number of rows that are now redundant.
    dimension_type num_redundant = 0;
    for (dimension_type row = space_dim; row > new_dimension; --row)
      if (dim_kinds[row] != CON_VIRTUAL)
        ++num_redundant;
    if (num_redundant > 0) {
      dimension_type rows = con_sys.num_rows();
      // Shuffle the remaining rows upwards.
      for (dimension_type low = 0,
             high = num_redundant; high < rows; ++high, ++low) {
        using std::swap;
        swap(con_sys[low], con_sys[high]);
      }
      // Chop newly redundant rows from end of system, to keep minimal
      // form.
      con_sys.remove_trailing_rows(num_redundant);
    }
    dim_kinds.resize(new_dimension + 1);
    clear_generators_up_to_date();
    // Replace gen_sys with an empty system of the right dimension.
    // Extra 2 columns for inhomogeneous term and modulus.
    Grid_Generator_System gs(new_dimension + 2);
    gen_sys.m_swap(gs);
  }

  // Update the space dimension.
  space_dim = new_dimension;

  PPL_ASSERT(OK(true));
}

void Parma_Polyhedra_Library::Grid::remove_space_dimensions ( const Variables_Set & vars )

Removes all the specified dimensions from the vector space.

Parameters:

vars	The set of Variable objects corresponding to the space dimensions to be removed.

Exceptions:

std::invalid_argument Thrown if *this is dimension-incompatible with one of the Variable objects contained in vars.

Definition at line 265 of file Grid_chdims.cc.

References PPL_ASSERT, and Parma_Polyhedra_Library::Variables_Set::space_dimension().

                                                          {
  // The removal of no dimensions from any grid is a no-op.  This case
  // also captures the only legal removal of dimensions from a grid in
  // a 0-dim space.
  if (vars.empty()) {
    PPL_ASSERT(OK());
    return;
  }

  // Dimension-compatibility check.
  const dimension_type min_space_dim = vars.space_dimension();
  if (space_dim < min_space_dim)
    throw_dimension_incompatible("remove_space_dimensions(vs)", min_space_dim);

  const dimension_type new_space_dim = space_dim - vars.size();

  if (marked_empty()
      || (!generators_are_up_to_date() && !update_generators())) {
    // Update the space dimension.
    space_dim = new_space_dim;
    set_empty();
    PPL_ASSERT(OK());
    return;
  }

  // Removing _all_ dimensions from a non-empty grid obtains the
  // zero-dimensional universe grid.
  if (new_space_dim == 0) {
    set_zero_dim_univ();
    return;
  }

  gen_sys.remove_space_dimensions(vars);

  clear_congruences_up_to_date();
  clear_generators_minimized();

  // Update the space dimension.
  space_dim = new_space_dim;

  PPL_ASSERT(OK(true));
}

template<typename M , typename R >

bool Parma_Polyhedra_Library::Grid::rows_are_zero	(	M &	system,
		dimension_type	first,
		dimension_type	last,
		dimension_type	row_size
	)

staticprivate

Checks that trailing rows contain only zero terms.

If all columns contain zero in the rows of system from row index first to row index last then return true, else return false. row_size gives the number of columns in each row.

This method is only used in assertions in the simplify methods.

Definition at line 237 of file Grid_simplify.cc.

                                                                  {
  while (first <= last) {
    const R& row = system[first++];
    for (dimension_type col = 0; col < row_size; ++col)
      if (row[col] != 0)
        return false;
  }
  return true;
}

void Parma_Polyhedra_Library::Grid::select_wider_congruences	(	const Grid &	y,
		Congruence_System &	selected_cgs
	)		const

private

Copies a widened selection of congruences from y to selected_cgs.

Definition at line 33 of file Grid_widenings.cc.

References con_sys, CON_VIRTUAL, congruences_are_minimized(), dim_kinds, EQUALITY, Parma_Polyhedra_Library::Congruence_System::insert(), Parma_Polyhedra_Library::Congruence::is_equal_at_dimension(), marked_empty(), PPL_ASSERT, PROPER_CONGRUENCE, space_dim, and Parma_Polyhedra_Library::Congruence_System::space_dimension().

Referenced by congruence_widening_assign().

                                                                           {
  // Private method: the caller must ensure the following conditions
  // (beside the inclusion `y <= x').
  PPL_ASSERT(space_dim == y.space_dim);
  PPL_ASSERT(!marked_empty());
  PPL_ASSERT(!y.marked_empty());
  PPL_ASSERT(congruences_are_minimized());
  PPL_ASSERT(y.congruences_are_minimized());

  // Note: row counters start at 0, to preserve the original order in
  // the selected congruences.
  for (dimension_type dim = con_sys.space_dimension(), x_row = 0, y_row = 0;
       dim > 0; --dim) {
    PPL_ASSERT(dim_kinds[dim] == CON_VIRTUAL
           || dim_kinds[dim] == y.dim_kinds[dim]);
    switch (dim_kinds[dim]) {
    case PROPER_CONGRUENCE:
      {
        const Congruence& cg = con_sys[x_row];
        const Congruence& y_cg = y.con_sys[y_row];
        if (cg.is_equal_at_dimension(dim, y_cg))
          // The leading diagonal entries are equal.
          selected_cgs.insert(cg);
        ++x_row;
        ++y_row;
      }
      break;
    case EQUALITY:
      selected_cgs.insert(con_sys[x_row]);
      ++x_row;
      ++y_row;
      break;
    case CON_VIRTUAL:
      if (y.dim_kinds[dim] != CON_VIRTUAL)
        ++y_row;
      break;
    }
  }
}

void Parma_Polyhedra_Library::Grid::select_wider_generators	(	const Grid &	y,
		Grid_Generator_System &	widened_ggs
	)		const

private

Copies widened generators from y to widened_ggs.

Definition at line 215 of file Grid_widenings.cc.

References Parma_Polyhedra_Library::Grid_Generator::coefficient(), dim_kinds, gen_sys, generators_are_minimized(), Parma_Polyhedra_Library::Grid_Generator_System::insert(), Parma_Polyhedra_Library::Grid_Generator::is_equal_at_dimension(), marked_empty(), PPL_ASSERT, space_dim, and Parma_Polyhedra_Library::Grid_Generator::space_dimension().

Referenced by generator_widening_assign().

                                                                             {
  // Private method: the caller must ensure the following conditions
  // (beside the inclusion `y <= x').
  PPL_ASSERT(space_dim == y.space_dim);
  PPL_ASSERT(!marked_empty());
  PPL_ASSERT(!y.marked_empty());
  PPL_ASSERT(generators_are_minimized());
  PPL_ASSERT(y.generators_are_minimized());

  // Note: row counters start at 0, to preserve the original order in
  // the selected generators.
  for (dimension_type dim = 0, x_row = 0, y_row = 0;
       dim <= gen_sys.space_dimension(); ++dim) {
    PPL_ASSERT(dim_kinds[dim] == LINE
           || y.dim_kinds[dim] == GEN_VIRTUAL
           || dim_kinds[dim] == y.dim_kinds[dim]);
    switch (dim_kinds[dim]) {
    case PARAMETER:
      {
        const Grid_Generator& gg = gen_sys[x_row];
        const Grid_Generator& y_gg = y.gen_sys[y_row];
        if (gg.is_equal_at_dimension(dim, y_gg))
          // The leading diagonal entry is equal.
          widened_ggs.insert(gg);
        else {
          Linear_Expression e;
          for (dimension_type i = gg.space_dimension(); i-- > 0; )
            e += gg.coefficient(Variable(i)) * Variable(i);
          widened_ggs.insert(grid_line(e));
        }
        ++x_row;
        ++y_row;
      }
      break;
    case LINE:
      widened_ggs.insert(gen_sys[x_row]);
      ++x_row;
      ++y_row;
      break;
    case GEN_VIRTUAL:
      if (y.dim_kinds[dim] != GEN_VIRTUAL)
        ++y_row;
      break;
    }
  }
}

void Parma_Polyhedra_Library::Grid::set_congruences_minimized ( )

inlineprivate

Sets status to express that congruences are minimized.

Definition at line 70 of file Grid.inlines.hh.

References Parma_Polyhedra_Library::Grid::Status::set_c_minimized(), set_congruences_up_to_date(), and status.

Referenced by congruence_widening_assign(), construct(), Parma_Polyhedra_Library::Grid_Certificate::Grid_Certificate(), is_empty(), minimize(), minimized_congruences(), and update_generators().

                                {
  set_congruences_up_to_date();
  status.set_c_minimized();
}

void Parma_Polyhedra_Library::Grid::set_congruences_up_to_date ( )

inlineprivate

Sets status to express that congruences are up-to-date.

Definition at line 65 of file Grid.inlines.hh.

References Parma_Polyhedra_Library::Grid::Status::set_c_up_to_date(), and status.

Referenced by Grid(), and set_congruences_minimized().

                                 {
  status.set_c_up_to_date();
}

void Parma_Polyhedra_Library::Grid::set_empty ( )

private

Sets status to express that the grid is empty, clearing all corresponding matrices.

Definition at line 448 of file Grid_nonpublic.cc.

References Parma_Polyhedra_Library::Congruence_System::increase_space_dimension(), and Parma_Polyhedra_Library::Congruence::zero_dim_false().

Referenced by congruence_widening_assign(), difference_assign(), Grid(), grid_generators(), intersection_assign(), is_empty(), map_space_dimensions(),

Classes

Public Types

Public Member Functions

Static Public Member Functions

Private Types

Private Member Functions

Static Private Member Functions

Private Attributes

Friends

Related Functions

Exception Throwers

Detailed Description

Member Typedef Documentation

Member Enumeration Documentation

Constructor & Destructor Documentation

Member Function Documentation