PPL Prolog Language Interface
1.2

The structure of this section is as follows:
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.
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:
ppl_new_C_Polyhedron_from_space_dimension(+Dimension_Type, +Universe_or_Empty, Handle)
Builds a new C polyhedron 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 . Thus the query
creates the C polyhedron defining the 3dimensional vector space 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
.
Besides the constructors listed above, the library also provides:
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
.
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.
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
.
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
.
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.
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.
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 nonstrict 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 nonstrict 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
.
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
toPPL_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
toPPL_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
PPL_Var
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
PPL_Var
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
Lin_Expr/
where is the symbol represented by Coeff
,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
Lin_Expr/
where is the symbol represented by Coeff
,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
Lin_Expr_2
, where 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
Lin_Expr_2
, where is the symbol represented by Relation_Symbol
.
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 polyhull 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 polydifference 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 nonempty. Assigns to P_1
its meetpreserving 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.
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 BHRZ03widening 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 H79widening 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 BHRZ03widening 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 H79widening 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 BHRZ03widening 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 BHRZ03widening 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 H79widening 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 H79widening 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 BHRZ03widening 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 BHRZ03widening 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 H79widening 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 H79widening 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
.
These predicates enable the modification of the vector space of the polyhedron referred to in the first argument.
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
.
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_Varth
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.
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.
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).
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, CertificateBased 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 BHZ03widening between P_1
and the pointset powerset referenced by Handle_2
, using the BHRZ03widening 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 BHZ03widening between P_1
and the pointset powerset referenced by Handle_2
, using the H79widening 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 BHRZ03widening 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 H79widening and the cardinality threshold C_unsigned
.