The structure of this section is as follows:

Predicates for the C Polyhedron Domain

Here we provide a short description for each of the predicates available for the domain of C polyhedra. Note that predicates for other domains will follow a similar pattern.

Constructor, copy, conversion and destructor predicates

Constructor predicates for C polyhedra

The constructor predicates build a C polyhedron from a specification and binds the given variable to a handle for future referencing. The specification can be:

the number of space dimensions and an atom indicating if it is to be the universe or empty element.
a representation for the particular class of semantic geometric descriptors to which the element being built belongs. For example, a C Polyhedron can be built from a list of non-strict inequality or equality constraints or a list of equality congruences or a list of generators that contains no closure points.

ppl_new_C_Polyhedron_from_space_dimension(+Dimension_Type, +Universe_or_Empty, -Handle)
Builds a new C polyhedron $\cP$ with Dimension_Type dimensions; it is empty or the universe depending on whether Atom is empty or universe, respectively. Handle is unified with the handle for $\cP$ . Thus the query

?- ppl_new_C_Polyhedron_from_space_dimension(3, universe, X).

creates the C polyhedron defining the 3-dimensional vector space $\Rset^3$ with X bound to a valid handle for accessing it.

ppl_new_C_Polyhedron_from_constraints(+Constraint_System, -Handle)
Builds a new C polyhedron P from Constraint_System. Handle is unified with the handle for P.

ppl_new_C_Polyhedron_from_congruences(+Congruence_System, -Handle)
Builds a new C polyhedron P from Congruence_System. Handle is unified with the handle for P.

ppl_new_C_Polyhedron_from_generators(+Generator_System, -Handle)
Builds a new C polyhedron P from Generator_System. Handle is unified with the handle for P.

Predicates that build new C polyhedra by copying or converting from other semantic geometric descriptions

Besides the constructors listed above, the library also provides:

copy constructors that will copy an element belonging to the same class of semantic geometric descriptions
conversion operators that build a new semantic geometric description starting from a friend; that is, a semantic geometric description in different class (e.g., ppl_new_Grid_from_C_Polyhedron, ppl_new_C_Polyhedron_from_BD_Shape_mpq_class, etc.).

The copy and conversion predicates have two versions, one with arity 2 for the source and target handles and one with an extra argument denoting the maximum complexity to be used in the conversion; this complexity argument is ignored when the the friend and the element being built are in the same class.

ppl_new_C_Polyhedron_from_C_Polyhedron(+Handle_1, -Handle_2)
Builds a new C polyhedron P_1 from the c polyhedron referenced by handle Handle_1. Handle_2 is unified with the handle for P_1.

ppl_new_C_Polyhedron_from_NNC_Polyhedron(+Handle_1, -Handle_2)
Builds a new C polyhedron P_1 from the nnc polyhedron referenced by handle Handle_1. Handle_2 is unified with the handle for P_1.

ppl_new_C_Polyhedron_from_C_Polyhedron_with_complexity(+Handle, +Complexity, -Handle)
Builds a new C polyhedron P_1 from the c polyhedron referenced by handle Handle_1 using an algorithm whose complexity does not exceed Complexity; Handle_2 is unified with the handle for P_1.

ppl_new_C_Polyhedron_from_NNC_Polyhedron_with_complexity(+Handle, +Complexity, -Handle)
Builds a new C polyhedron P_1 from the nnc polyhedron referenced by handle Handle_1 using an algorithm whose complexity does not exceed Complexity; Handle_2 is unified with the handle for P_1.

Destructor predicate

Below is the destructor predicate for the Polyhedron domain.

ppl_delete_Polyhedron(+Handle)
Invalidates the handle referenced by Handle: this makes sure the corresponding resources will eventually be released.

Predicates that do not change the polyhedron

Test Predicates

These predicates test the polyhedron for different properties and succeed or fail depending on the outcome.

ppl_Polyhedron_is_empty(+Handle)
Succeeds if and only if the polyhedron referenced by Handle is empty.

ppl_Polyhedron_is_universe(+Handle)
Succeeds if and only if the polyhedron referenced by Handle is the universe.

ppl_Polyhedron_is_bounded(+Handle)
Succeeds if and only if the polyhedron referenced by Handle is bounded.

ppl_Polyhedron_contains_integer_point(+Handle)
Succeeds if and only if the polyhedron referenced by Handle contains an integer point.

ppl_Polyhedron_is_topologically_closed(+Handle)
Succeeds if and only if the polyhedron referenced by Handle is topologically closed.

ppl_Polyhedron_is_discrete(+Handle)
Succeeds if and only if the polyhedron referenced by Handle is discrete.

ppl_Polyhedron_bounds_from_above(+Handle, +Lin_Expr)
Succeeds if and only if Lin_Expr is bounded from above in the polyhedron referenced by Handle.

ppl_Polyhedron_bounds_from_below(+Handle, +Lin_Expr)
Succeeds if and only if Lin_Expr is bounded from below in the polyhedron referenced by Handle.

ppl_Polyhedron_contains_Polyhedron(+Handle_1, +Handle_2)
Succeeds if and only if the polyhedron referenced by Handle_2 is included in or equal to the polyhedron referenced by Handle_1.

ppl_Polyhedron_strictly_contains_Polyhedron(+Handle_1, +Handle_2)
Succeeds if and only if the polyhedron referenced by Handle_2 is included in but not equal to the polyhedron referenced by Handle_1.

ppl_Polyhedron_is_disjoint_from_Polyhedron(+Handle_1, +Handle_2)
Succeeds if and only if the polyhedron referenced by Handle_2 is disjoint from the polyhedron referenced by Handle_1.

ppl_Polyhedron_equals_Polyhedron(+Handle_1, +Handle_2)
Succeeds if and only if the polyhedron referenced by Handle_1 is equal to the polyhedron referenced by Handle_2.

ppl_Polyhedron_OK(+Handle)
Succeeds only if the polyhedron referenced by Handle is well formed, i.e., if it satisfies all its implementation invariants. Useful for debugging purposes.

ppl_Polyhedron_constrains(+Handle, +PPL_Var)
Succeeds if and only if the polyhedron referenced by Handle constrains the dimension PPL_Var.

Predicates that return information about the polyhedron

These predicates will obtain more detailed information about the polyhedron unifying some of their arguments with the results.

ppl_Polyhedron_space_dimension(+Handle, ?Dimension_Type)
Unifies Dimension_Type with the dimension of the vector space enclosing the polyhedron referenced by Handle.

ppl_Polyhedron_affine_dimension(+Handle, ?Dimension_Type)
Unifies Dimension_Type with the affine dimension of the polyhedron referenced by Handle.

ppl_Polyhedron_relation_with_constraint(+Handle, +Constraint, ?Relation_List)
Unifies Relation_List with the list of relations the polyhedron referenced by Handle has with Constraint. The possible relations are listed in the grammar rules above.

ppl_Polyhedron_relation_with_generator(+Handle, +Generator, ?Relation_List)
Unifies Relation_List with the list of relations the polyhedron referenced by Handle has with Generator. The possible relations are listed in the grammar rules above.

ppl_Polyhedron_relation_with_congruence(+Handle, +Congruence, ?Relation_List)
Unifies Relation_List with the list of relations the polyhedron referenced by Handle has with Congruence. The possible relations are listed in the grammar rules above.

ppl_Polyhedron_get_constraints(+Handle, ?Constraint_System)
Unifies Constraint_System with the constraints (in the form of a list) in the constraint system satisfied by the polyhedron referenced by Handle.

ppl_Polyhedron_get_congruences(+Handle, ?Congruence_System)
Unifies Congruence_System with the congruences (in the form of a list) in the congruence system satisfied by the polyhedron referenced by Handle.

ppl_Polyhedron_get_generators(+Handle, ?Generator_System)
Unifies Generator_System with the generators (in the form of a list) in the generator system for the polyhedron referenced by Handle.

ppl_Polyhedron_get_minimized_constraints(+Handle, ?Constraint_System)
Unifies Constraint_System with the constraints (in the form of a list) in the minimized constraint system satisfied by the polyhedron referenced by Handle.

ppl_Polyhedron_get_minimized_congruences(+Handle, ?Congruence_System)
Unifies Congruence_System with the congruences (in the form of a list) in the minimized congruence system for the polyhedron referenced by Handle.

ppl_Polyhedron_get_minimized_generators(+Handle, ?Generator_System)
Unifies Generator_System with the generators (in the form of a list) in the minimized generator system satisfied by the polyhedron referenced by Handle.

ppl_Polyhedron_maximize(+Handle, +Lin_Expr, ?Coeff_1, ?Coeff_2, ?Boolean)
Succeeds if and only if polyhedron P referenced by Handle is not empty and Lin_Expr is bounded from above in P.

Coeff_1 is unified with the numerator of the supremum value and Coeff_2 with the denominator of the supremum value. If the supremum is also the maximum, Boolean is unified with the atom true and, otherwise, unified with the atom false.

ppl_Polyhedron_minimize(+Handle, +Lin_Expr, ?Coeff_1, ?Coeff_2, ?Boolean)
Succeeds if and only if polyhedron P referenced by Handle is not empty and Lin_Expr is bounded from below in P.

Coeff_1 is unified with the numerator of the infinum value and Coeff_2 with the denominator of the infinum value. If the infinum is also the minimum, Boolean is unified with the atom true and, otherwise, unified with the atom false.

ppl_Polyhedron_maximize_with_point(+Handle, +Lin_Expr, ?Coeff_1, ?Coeff_2, ?Boolean, ?Point)
Succeeds if and only if polyhedron P referenced by Handle is not empty and Lin_Expr is bounded from above in P.

Coeff_1 is unified with the numerator of the supremum value and Coeff_2 with the denominator of the supremum value and Point with a point or closure point where Lin_Expr reaches this value. If the supremum is also the maximum, Boolean is unified with the atom true and, otherwise, unified with the atom false.

ppl_Polyhedron_minimize_with_point(+Handle, +Lin_Expr, ?Coeff_1, ?Coeff_2, ?Boolean, ?Point)
Succeeds if and only if polyhedron P referenced by Handle is not empty and Lin_Expr is bounded from below in P.

Coeff_1 is unified with the numerator of the infinum value and Coeff_2 with the denominator of the infinum value and Point with a point or closure point where Lin_Expr reaches this value. If the infinum is also the minimum, Boolean is unified with the atom true and, otherwise, unified with the atom false.

ppl_Polyhedron_external_memory_in_bytes(+Handle, ?Number)
Unifies Number with the size of the total memory in bytes occupied by the polyhedron referenced by Handle.

ppl_Polyhedron_total_memory_in_bytes(+Handle, ?Number)
Unifies Number with the size of the external memory in bytes occupied by the polyhedron referenced by Handle.

Ascii dump predicate

This output predicate is useful for debugging.

ppl_Polyhedron_ascii_dump(+Handle)
Dumps an ascii representation of the PPL internal state for the polyhedron referenced by Handle on the standard output.

Space-dimension preserving predicates that may change the polyhedron

These predicates may modify the polyhedron referred to by the handle in first argument; the (dimension of the) vector space in which it is embedded is unchanged.

Predicates that may change the polyhedron by adding to its constraint or generator descriptions

Note that there are two forms of these predicates differentiated in the names by the words "add" or "refine with"; see Section Generic Operations on Semantic Geometric Descriptors in the main PPL User Manual for the differences in the semantics and therefore, the expected behavior, between these forms.

ppl_Polyhedron_add_constraint(+Handle, +Constraint)
Updates the polyhedron referenced by Handle to one obtained by adding Constraint to its constraint system. For a C polyhedron, Constraint must be an equality or a non-strict inequality.

ppl_Polyhedron_add_congruence(+Handle, +Congruence)
Updates the polyhedron referenced by Handle to one obtained by adding Congruence to its congruence system. For a C polyhedron, Congruence must be an equality.

ppl_Polyhedron_add_generator(+Handle, +Generator)
Updates the polyhedron referenced by Handle to one obtained by adding Generator to its generator system. For a C polyhedron, Generator must be a line, ray or point.

ppl_Polyhedron_add_constraints( +Handle, +Constraint_System)
Updates the polyhedron referenced by Handle to one obtained by adding to its constraint system the constraints in Constraint_System. For a C polyhedron, Constraints must be a list of equalities and non-strict inequalities.

ppl_Polyhedron_add_congruences( +Handle, +Congruence_System)
Updates the polyhedron referenced by Handle to one obtained by adding to its congruence system the congruences in Congruence_System. For a C polyhedron, Congruences must be a list of equalities.

ppl_Polyhedron_add_generators( +Handle, +Generator_System)
Updates the polyhedron referenced by Handle to one obtained by adding to its generator system the generators in Generator_System. For a C polyhedron, Generators must be a list of lines, rays and points.

ppl_Polyhedron_refine_with_constraint( +Handle, +Constraint)
Updates the polyhedron referenced by Handle to one obtained by refining its constraint system with Constraint.

ppl_Polyhedron_refine_with_congruence( +Handle, +Congruence)
Updates the polyhedron referenced by Handle to one obtained by refining its congruence system with Congruence.

ppl_Polyhedron_refine_with_constraints( +Handle, +Constraint_System)
Updates the polyhedron referenced by Handle to one obtained by refining its constraint system with the constraints in Constraint_System.

ppl_Polyhedron_refine_with_congruences( +Handle, +Congruence_System)
Updates the polyhedron referenced by Handle to one obtained by refining its congruence system with the congruences in Congruence_System.

Predicates that transform the polyhedron

These predicates enable transformations such as taking the topological closure (which for the domain of C polyhedron is the identity transformation), unconstraining a specified dimension as explained in the main PPL User Manual in Section Cylindrification Operator and several different image and preimage affine transfer relations; for details of the latter see Sections Images and Preimages of Affine Transfer Relations and Generalized Affine Relations

ppl_Polyhedron_topological_closure_assign(+Handle)
Assigns to the polyhedron referenced by Handle its topological closure.

ppl_Polyhedron_unconstrain_space_dimension(+Handle, +PPL_Var)
Modifies the polyhedron P referenced by Handle by unconstraining the space dimension PPL_Var.

ppl_Polyhedron_unconstrain_space_dimensions(+Handle, +List_of_PPL_Var)
Modifies the polyhedron P referenced by Handle by unconstraining the space dimensions that are specified in List_of_PPL_Var. The presence of duplicates in List_of_PPL_Var is a waste but an innocuous one.

ppl_Polyhedron_affine_image(+Handle, +PPL_Var, +Lin_Expr, +Coeff)
Transforms the polyhedron referenced by Handle assigning the affine expression for Lin_Expr/Coeff to PPL_Var.

ppl_Polyhedron_affine_preimage(+Handle, +PPL_Var, +Lin_Expr, +Coeff)
Transforms the polyhedron referenced by Handle substituting the affine expression for Lin_Expr/Coeff to PPL_Var.

ppl_Polyhedron_bounded_affine_image(+Handle, +PPL_Var, +Lin_Expr_1, +Lin_Expr_2, +Coeff)
Assigns to polyhedron P referenced by Handle the generalized image with respect to the generalized affine transfer relation Lin_Expr_1/Coeff $\leq$ PPL_Var $\leq$ Lin_Expr_2/Coeff.

ppl_Polyhedron_bounded_affine_preimage(+Handle, +PPL_Var, +Lin_Expr_1, +Lin_Expr_2, +Coeff)
Assigns to polyhedron P referenced by Handle the generalized preimage with respect to the generalized affine transfer relation Lin_Expr_1/Coeff $\leq$ PPL_Var $\leq$ Lin_Expr_2/Coeff.

ppl_Polyhedron_generalized_affine_image(+Handle, +PPL_Var, +Relation_Symbol, +Lin_Expr, +Coeff)
Assigns to polyhedron P referenced by Handle the generalized image with respect to the generalized affine transfer relation PPL_Var $\bowtie$ Lin_Expr/Coeff, where $\bowtie$ is the symbol represented by Relation_Symbol.

ppl_Polyhedron_generalized_affine_preimage(+Handle, +PPL_Var, +Relation_Symbol, +Lin_Expr, +Coeff)
Assigns to polyhedron P referenced by Handle the generalized preimage with respect to the generalized affine transfer relation PPL_Var $\bowtie$ Lin_Expr/Coeff, where $\bowtie$ is the symbol represented by Relation_Symbol.

ppl_Polyhedron_generalized_affine_image_lhs_rhs(+Handle, +Lin_Expr_1, +Relation_Symbol, +Lin_Expr_2)
Assigns to polyhedron P referenced by Handle the generalized image with respect to the generalized affine transfer relation Lin_Expr_1 $\bowtie$ Lin_Expr_2, where $\bowtie$ is the symbol represented by Relation_Symbol.

ppl_Polyhedron_generalized_affine_preimage_lhs_rhs(+Handle, +Lin_Expr_1, +Relation_Symbol, +Lin_Expr_2)
Assigns to polyhedron P referenced by Handle the generalized preimage with respect to the generalized affine transfer relation Lin_Expr_1 $\bowtie$ Lin_Expr_2, where $\bowtie$ is the symbol represented by Relation_Symbol.

Predicates whose results depend on more than one polyhedron

These predicates include the binary operators which will assign to the polyhedron referred to by the first argument its combination with the polyhedron referred to by the second argument as described in the main PPL User Manual in Sections Intersection and Convex Polyhedral Hull and Convex Polyhedral Difference; and a linear partitioning operator described below.

ppl_Polyhedron_intersection_assign(+Handle_1, +Handle_2)
Assigns to the polyhedron P referenced by Handle_1 the intersection of P and the polyhedron referenced by Handle_2.

ppl_Polyhedron_upper_bound_assign(+Handle_1, +Handle_2)
Assigns to the polyhedron P referenced by Handle_1 the upper bound of P and the polyhedron referenced by Handle_2.

ppl_Polyhedron_difference_assign(+Handle_1, +Handle_2)
Assigns to the polyhedron P referenced by Handle_1 the difference of P and the polyhedron referenced by Handle_2.

ppl_Polyhedron_time_elapse_assign(+Handle_1, +Handle_2)
Assigns to the polyhedron P referenced by Handle_1 the time elapse of P and the polyhedron referenced by Handle_2.

ppl_Polyhedron_poly_hull(+Handle_1, +Handle_2)
Assigns to the polyhedron P referenced by Handle_1 the poly-hull of P and the polyhedron referenced by Handle_2.

ppl_Polyhedron_poly_difference(+Handle_1, +Handle_2)
Assigns to the polyhedron P referenced by Handle_1 the poly-difference of P and the polyhedron referenced by Handle_2.

ppl_Polyhedron_upper_bound_assign_if_exact(+Handle_1, +Handle_2)
Succeeds if the least upper bound of the polyhedron P_1 referenced by Handle_1 with the polyhedron referenced by Handle_2 is exact; in which case the least upper bound is assigned to P_1; fails otherwise.

ppl_Polyhedron_poly_hull_assign_if_exact(+Handle_1, +Handle_2)
Succeeds if the least upper bound of the polyhedron P_1 referenced by Handle_1 with the polyhedron referenced by Handle_2 is exact; in which case the least upper bound is assigned to P_1; fails otherwise.

ppl_Polyhedron_simplify_using_context_assign(+Handle_1, +Handle_2, ?Boolean)
Succeeds if and only if the intersection of polyhedron P_1 referenced by Handle_1 and the polyhedron P_2 referenced by Handle_2 is non-empty. Assigns to P_1 its meet-preserving simplification with respect to P_2.

ppl_Polyhedron_linear_partition(+Handle_1, +Handle_2, -Handle_3, -Handle_4)
Handle_1 and Handle_2 are handles for elements P_1 and P_2 in the Polyhedron domain. The predicate unifies handle Handle_3 to a reference to the intersection of P_1 and P_2 and Handle_4 to a reference to a pointset powerset of nnc polyhedra P_4; where P_4 is the linear partition of P_1 with respect to P_2. This predicate is only provided if the class Pointset_Powerset_NNC_Polyhedron has been enabled when configuring the library.

Predicates for widening and extrapolation

In addition to the above binary operators, there are also a number of widening, extrapolation and narrowing operators as described in the main PPL User Manual in Sections Widening Operators, Widening with Tokens and Extrapolation Operators. Note that for all these widening and extrapolation predicates to behave as specified the polyhedron referred to by the second argument has to be contained in (or equal to) the polyhedron referred to by the first argument.

ppl_Polyhedron_BHRZ03_widening_assign_with_tokens(+Handle_1, +Handle_2, +C_unsigned_1, ?C_unsigned_2)
Assigns to the polyhedron P_1 referenced by Handle_1 the BHRZ03-widening of P_1 with the polyhedron referenced by Handle_2. The widening with tokens delay technique is applied with C_unsigned_1 tokens; C_unsigned_2 is unified with the number of tokens remaining at the end of the operation.

ppl_Polyhedron_H79_widening_assign_with_tokens(+Handle_1, +Handle_2, +C_unsigned_1, ?C_unsigned_2)
Assigns to the polyhedron P_1 referenced by Handle_1 the H79-widening of P_1 with the polyhedron referenced by Handle_2. The widening with tokens delay technique is applied with C_unsigned_1 tokens; C_unsigned_2 is unified with the number of tokens remaining at the end of the operation.

ppl_Polyhedron_BHRZ03_widening_assign(+Handle_1, +Handle_2)
Assigns to the polyhedron P_1 referenced by Handle_1 the BHRZ03-widening of P_1 with the polyhedron referenced by Handle_2.

ppl_Polyhedron_H79_widening_assign(+Handle_1, +Handle_2)
Assigns to the polyhedron P_1 referenced by Handle_1 the H79-widening of P_1 with the polyhedron referenced by Handle_2.

ppl_Polyhedron_widening_assign_with_tokens(+Handle_1, +Handle_2, +C_unsigned_1, ?C_unsigned_2)
Same as predicate ppl_Polyhedron_H79_widening_assign_with_tokens/4

ppl_Polyhedron_widening_assign(+Handle_1, +Handle_2)
Same as predicate ppl_Polyhedron_H79_widening_assign/2

ppl_Polyhedron_limited_BHRZ03_extrapolation_assign_with_tokens(+Handle_1, +Handle_2, +Constraint_System, +C_unsigned_1, ?C_unsigned_2)
Assigns to the polyhedron P_1 referenced by Handle_1 the BHRZ03-widening of P_1 with the polyhedron referenced by Handle_2 intersected with the constraints in Constraint_System that are satisfied by all the points of P_1. The widening with tokens delay technique is applied with C_unsigned_1 tokens; C_unsigned_2 is unified with the number of tokens remaining at the end of the operation.

ppl_Polyhedron_bounded_BHRZ03_extrapolation_assign_with_tokens(+Handle_1, +Handle_2, +Constraint_System, +C_unsigned_1, ?C_unsigned_2)
Assigns to the polyhedron P_1 referenced by Handle_1 the BHRZ03-widening of P_1 with the polyhedron referenced by Handle_2 intersected with the constraints in Constraint_System that are satisfied by all the points of P_1, further intersected with the smallest box containing P_1. The widening with tokens delay technique is applied with C_unsigned_1 tokens; C_unsigned_2 is unified with the number of tokens remaining at the end of the operation.

ppl_Polyhedron_limited_H79_extrapolation_assign_with_tokens(+Handle_1, +Handle_2, +Constraint_System, +C_unsigned_1, ?C_unsigned_2)
Assigns to the polyhedron P_1 referenced by Handle_1 the H79-widening of P_1 with the polyhedron referenced by Handle_2 intersected with the constraints in Constraint_System that are satisfied by all the points of P_1. The widening with tokens delay technique is applied with C_unsigned_1 tokens; C_unsigned_2 is unified with the number of tokens remaining at the end of the operation.

ppl_Polyhedron_bounded_H79_extrapolation_assign_with_tokens(+Handle_1, +Handle_2, +Constraint_System, +C_unsigned_1, ?C_unsigned_2)
Assigns to the polyhedron P_1 referenced by Handle_1 the H79-widening of P_1 with the polyhedron referenced by Handle_2 intersected with the constraints in Constraint_System that are satisfied by all the points of P_1, further intersected with the smallest box containing P_1. The widening with tokens delay technique is applied with C_unsigned_1 tokens; C_unsigned_2 is unified with the number of tokens remaining at the end of the operation.

ppl_Polyhedron_limited_BHRZ03_extrapolation_assign(+Handle_1, +Handle_2, +Constraint_System)
Assigns to the polyhedron P_1 referenced by Handle_1 the BHRZ03-widening of P_1 with the polyhedron referenced by Handle_2 intersected with the constraints in Constraint_System that are satisfied by all the points of P_1.

ppl_Polyhedron_bounded_BHRZ03_extrapolation_assign(+Handle_1, +Handle_2, +Constraint_System)
Assigns to the polyhedron P_1 referenced by Handle_1 the BHRZ03-widening of P_1 with the polyhedron referenced by Handle_2 intersected with the constraints in Constraint_System that are satisfied by all the points of P_1, further intersected with the smallest box containing P_1.

ppl_Polyhedron_limited_H79_extrapolation_assign(+Handle_1, +Handle_2, +Constraint_System)
Assigns to the polyhedron P_1 referenced by Handle_1 the H79-widening of P_1 with the polyhedron referenced by Handle_2 intersected with the constraints in Constraint_System that are satisfied by all the points of P_1.

ppl_Polyhedron_bounded_H79_extrapolation_assign(+Handle_1, +Handle_2, +Constraint_System)
Assigns to the polyhedron P_1 referenced by Handle_1 the H79-widening of P_1 with the polyhedron referenced by Handle_2 intersected with the constraints in Constraint_System that are satisfied by all the points of P_1, further intersected with the smallest box containing P_1.

Predicates that may modify the vector space

These predicates enable the modification of the vector space of the polyhedron referred to in the first argument.

Predicate for concatenation

For more information on this operation, see Section Concatenating Polyhedra, of the main PPL User Manual.

ppl_Polyhedron_concatenate_assign(+Handle_1, +Handle_2)
Assigns to the polyhedron P referenced by Handle_1 the concatenation of P and the polyhedron referenced by Handle_2.

Predicates for mapping dimensions or changing the vector space

These predicates enable the modification of the vector space of the polyhedron referred to in the first argument. These predicates enable the modification of the vector space of the polyhedron referred to in the first argument. Detailed descriptions of these can be found in the main PPL User Manual in Sections Adding New Dimensions to the Vector Space, Removing Dimensions from the Vector Space, Mapping the Dimensions of the Vector Space, Expanding One Dimension of the Vector Space to Multiple Dimensions and Folding Multiple Dimensions of the Vector Space into One Dimension.

ppl_Polyhedron_add_space_dimensions_and_embed(+Handle, +Dimension_Type)
Adds Dimension_Type new dimensions to the space enclosing the polyhedron P referenced by Handle and and_embeds P in this space.

ppl_Polyhedron_add_space_dimensions_and_project(+Handle, +Dimension_Type)
Adds Dimension_Type new dimensions to the space enclosing the polyhedron P referenced by Handle and and_projects P in this space.

ppl_Polyhedron_remove_space_dimensions(+Handle, +List_of_PPL_Vars)
Removes from the vector space enclosing the polyhedron P referenced by Handle the space dimensions that are specified in List_of_PPL_Var. The presence of duplicates in List_of_PPL_Var is a waste but an innocuous one.

ppl_Polyhedron_remove_higher_space_dimensions(+Handle, +Dimension_Type)
Removes the higher dimensions from the vector space enclosing the polyhedron P referenced by Handle so that, upon successful return, the new space dimension is Dimension_Type.

ppl_Polyhedron_expand_space_dimension(+Handle, +PPL_Var, +Dimension_Type)
Expands the PPL_Var-th dimension of the vector space enclosing the polyhedron referenced by Handle to Dimension_Type new space dimensions.

ppl_Polyhedron_fold_space_dimensions(+Handle, +List_of_PPL_Vars, +PPL_Var)
Modifies the polyhedron referenced by Handle by folding the space dimensions contained in List_of_PPL_Vars into dimension PPL_Var. The presence of duplicates in List_of_PPL_Vars is a waste but an innocuous one.

ppl_Polyhedron_map_space_dimensions(+Handle, +P_Func)
Remaps the dimensions of the vector space according to a partial function. This function is specified by means of the P_Func, which has n entries. The result is undefined if P_Func does not encode a partial function.

Ad hoc Predicates for Other Domains

Extra Predicates Specifically for the Pointset Powerset Domains

The powerset domains can be instantiated by taking as a base domain any fixed semantic geometric description (C and NNC polyhedra, BD and octagonal shapes, boxes and grids). An element of the powerset domain represents a disjunctive collection of base objects (its disjuncts), all having the same space dimension. For more information on this construct, see Section The Powerset Domain in the main PPL User Manual.

Besides the predicates that are available in all semantic geometric descriptions (whose documentation is not repeated here), the powerset domain also provides several ad hoc predicates. These are specified below, instantiated for the PPL domain Pointset_Powerset_C_Polyhedron. Note that predicates for other pointset powerset domains will follow similar patterns.

Predicates for pointset powerset iterators and disjuncts.

Iterators allow the user to examine and change individual elements (called here disjuncts) of a pointset powerset. Detailed descriptions for adding and removing disjuncts can be found in the main PPL User Manual in Section Adding a Disjunct. The following predicates support useful operations on these iterators and disjuncts via the usual handles.

ppl_new_Pointset_Powerset_C_Polyhedron_iterator_from_iterator(+Iterator_1, -Iterator_2)
Builds a new iterator it from the iterator referenced by Iterator_1. Iterator_2 is unified with the handle for it.

ppl_Pointset_Powerset_C_Polyhedron_begin_iterator(+Handle, -Iterator)
Unifies Iterator with a handle to an iterator "pointing" to the beginning of the sequence of disjuncts of the powerset referred to by Handle.

ppl_Pointset_Powerset_C_Polyhedron_end_iterator(+Handle, -Iterator)
Unifies Iterator with a handle to an iterator "pointing" to the end of the sequence of disjuncts of the powerset referred to by Handle.

ppl_Pointset_Powerset_C_Polyhedron_iterator_equals_iterator(+Iterator_1, +Iterator_2)
Succeeds if and only if the iterator referenced by Iterator_1 is equal to the iterator referenced by Iterator_2.

ppl_Pointset_Powerset_C_Polyhedron_iterator_increment(+Iterator)
Increments the iterator referenced by Iterator so that it "points" to the next disjunct.

ppl_Pointset_Powerset_C_Polyhedron_iterator_decrement(+Iterator)
Decrements the iterator referenced by Iterator so that it "points" to the previous disjunct.

ppl_Pointset_Powerset_C_Polyhedron_iterator_get_disjunct(+Iterator, -Handle)
Unifies with Handle a reference to the disjunct referred to by Iterator_1.

ppl_delete_Pointset_Powerset_C_Polyhedron_iterator(+Iterator)
Invalidates the handle referenced by Iterator: this makes sure the corresponding resources will eventually be released.

ppl_Pointset_Powerset_C_Polyhedron_add_disjunct(+Handle_1, +Handle_2)
Adds to the pointset powerset referenced by Handle_1 a disjunct referred to by Handle_2.

ppl_Pointset_Powerset_C_Polyhedron_drop_disjunct(+Handle, +Iterator)
If it is the iterator referred to by Iterator, drops from the pointset powerset referenced by Handle the disjunct pointed to by it and assigns to it an iterator to the next disjunct.

ppl_Pointset_Powerset_C_Polyhedron_drop_disjuncts(+Handle, +Iterator_1, +Iterator_2)
If it_1 and it_2 are the iterators referred to by Iterator_1 and Iterator_2, respectively, drops from the pointset powerset referenced by Handle all the disjuncts from it_1 to it_2 (excluded).

Other Ad Hoc Predicates for the pointset powerset domains.

Collected here are some other predicates that are specific to pointset powersets of C polyhedra; these provide operations for simplifying the powerset, geometric comparisons and widening and extrapolation. Detailed descriptions of these can be found in the main PPL User Manual in Sections Geometric Comparisons, Certificate-Based Widenings, Powerset Extrapolation Operators.

ppl_Pointset_Powerset_C_Polyhedron_pairwise_reduce(+Handle)
Assigns the result of pairwise reduction on the pointset powerset referenced by Handle.

ppl_Pointset_Powerset_C_Polyhedron_omega_reduce(+Handle)
Assigns the result of omega reduction on the pointset powerset referenced by Handle.

ppl_Pointset_Powerset_C_Polyhedron_geometrically_covers_Pointset_Powerset_C_Polyhedron(+Handle_1, +Handle_2)
Succeeds if and only if the pointset powerset referenced by Handle_2 geometrically covers the pointset powerset referenced by Handle_1; see Section Geometric Comparisons in the main PPL User Manual.

ppl_Pointset_Powerset_C_Polyhedron_geometrically_equals_Pointset_Powerset_C_Polyhedron(+Handle_1, +Handle_2)
Succeeds if and only if the pointset powerset referenced by Handle_2 geometrically equals the pointset powerset referenced by Handle_1; see Section Geometric Comparisons in the main PPL User Manual.

ppl_Pointset_Powerset_C_Polyhedron_BHZ03_BHRZ03_BHRZ03_widening_assign(+Handle_1, +Handle_2)
Assigns to the pointset powerset P_1 referenced by Handle_1 the BHZ03-widening between P_1 and the pointset powerset referenced by Handle_2, using the BHRZ03-widening certified by the convergence certificate for BHRZ03.

ppl_Pointset_Powerset_C_Polyhedron_BHZ03_H79_H79_widening_assign(+Handle_1, +Handle_2)
Assigns to the pointset powerset P_1 referenced by Handle_1 the BHZ03-widening between P_1 and the pointset powerset referenced by Handle_2, using the H79-widening certified by the convergence certificate for H79.

ppl_Pointset_Powerset_C_Polyhedron_BGP99_BHRZ03_extrapolation_assign(+Handle_1, +Handle_2, C_unsigned)
Assigns to the pointset powerset P_1 referenced by Handle_1 the result of applying the BGP99 extrapolation operator between P_1 and the pointset powerset referenced by Handle_2, using the BHRZ03-widening and the cardinality threshold C_unsigned.

ppl_Pointset_Powerset_C_Polyhedron_BGP99_H79_extrapolation_assign(+Handle_1, +Handle_2, C_unsigned)
Assigns to the pointset powerset P_1 referenced by Handle_1 the result of applying the BGP99 extrapolation operator between P_1 and the pointset powerset referenced by Handle_2, using the H79-widening and the cardinality threshold C_unsigned.