Generalities
The NDD package provides functions and datatypes for manipulating sets of unbounded integer vectors. The sets of vectors that can be represented by NDDs include those that can be expressed in Presburger arithmetic (i.e., the first-order arithmetic theory of integers without multiplication). The package provides functions for representing elementary sets and for performing various operations over represented sets.
In order to use the NDD package, one must link the application to the three following library files (all located in the lib/ subdirectory of the main LASH directory):- lash-core.o
- lash-arith.o
- ndd-package.o
Datatypes
The following datatypes are provided by the NDD package:ndd : Number Decision Diagram (representation of a set of integer vectors).
linear_transf : Linear transformation over integer vectors.
linear_tr_info : Object that can be associated to a linear transformation in order to speed up its application to sets represented by NDDs.
linear_star_info : Object that can be associated to a linear transformation in order to speed up the computation of its repeated effect.
Functions
The functions provided by the NDD package can be grouped into several categories:Functions for constructing elementary NDDs
ndd_create_empty, ndd_create_empty_lsdf, ndd_create_empty_msdf : Construct an NDD representing the empty set.
ndd_create_zn, ndd_create_zn_lsdf, ndd_create_zn_msdf : Construct an NDD representing the universal set.
ndd_create_eq2, ndd_create_eq2_lsdf, ndd_create_eq2_msdf : Construct an NDD representing the set of all the pairs with equal components.
ndd_create_equation, ndd_create_equation_lsdf, ndd_create_equation_msdf : Construct an NDD representing the set of solutions of a linear equation.
ndd_create_inequation, ndd_create_inequation_lsdf, ndd_create_inequation_msdf : Construct an NDD representing the set of solutions of a linear constraint.
Function for freeing NDDs
ndd_free : Unallocates an NDD.
Functions for combining and transforming NDDs
ndd_product : Computes the Cartesian product of two sets represented by NDDs.
ndd_difference : Computes the difference of two sets represented by NDDs.
ndd_union, ndd_merge : Compute the union of two sets represented by NDDs.
ndd_intersection : Computes the intersection of two sets represented by NDDs.
ndd_projection, ndd_multi_projection : Compute the projection of a set represented by an NDD over some vector components.
ndd_base_expand, ndd_base_reduce : Perform base-dependent operations over a set represented by an NDD.
ndd_interleave_z : Interleaves additional vector components in the elements of a set represented by an NDD.
Functions for testing NDDs
ndd_is_empty : Tests whether a set represented by an NDD is empty.
ndd_inclusion : Tests whether a set represented by an NDD is a subset of another set.
ndd_equality, ndd_disjoint : Test whether two sets represented by NDDs are equal to each other, or whether there are disjoint.
Functions related to linear transformations
ndd_create_transf : Constructs a linear transformation defined by its coefficients.
ndd_create_identity_transf : Constructs a linear transformation corresponding to the identity function.
ndd_create_assign_transf : Constructs a linear transformation corresponding to an assignment operation.
ndd_create_equ_transf, ndd_create_inequ_transf : Construct a linear transformation corresponding to an equality or inequality constraint.
ndd_transf_compose : Composes two linear transformations.
ndd_transf_power : Computes a power of a linear transformation.
ndd_transf_copy : Constructs a copy of a linear transformation.
ndd_transf_free : Unallocates a linear transformation.
ndd_image_by_transf : Computes the image by a linear transformation of a set represented by an NDD.
ndd_create_transf_info : Constructs an information structure associated to a linear transformation (in order to speed up its computation).
ndd_image_by_transf_info : Computes the image by a linear transformation information structure of a set represented by an NDD.
ndd_transf_info_free : Unallocates a linear transformation information structure.
Functions related to iterating linear transformations
ndd_definable_closure : Checks whether the unbounded repeated effect of a given linear transformation can be computed.
ndd_image_by_star_transf : Computes the image of a set represented by an NDD by the unbounded repetition of a linear transformation.
ndd_create_star_info : Constructs an information structure associated to the closure of a linear transformation (in order to speed up its computation).
ndd_image_by_star_info : Computes the image of a set represented by an NDD by a linear-transformation closure-information structure.
ndd_star_info_free : Unallocates a linear-transformation closure-information structure.