From 66d4b6136e0021128861fbdca9d301c7748dc222 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Mon, 25 Jan 2010 22:09:20 +0100 Subject: [PATCH] doc: describe input/output formats --- doc/user.pod | 80 +++++++++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 58 insertions(+), 22 deletions(-) diff --git a/doc/user.pod b/doc/user.pod index 9a967ea..ce0ca45 100644 --- a/doc/user.pod +++ b/doc/user.pod @@ -369,9 +369,48 @@ C (only for relations), C =head2 Input and Output -Proper input and output functions are still in development. -However, some functions are provided to read and write -to foreign file formats. +C supports its own input/output format, which is similar +to the C format, but also supports the C format +in some cases. + +=head3 C format + +The C format is similar to that of C, but has a different +syntax for describing the parameters and allows for the definition +of an existentially quantified variable as the integer division +of an affine expression. +For example, the set of integers C between C<0> and C +such that C can be described as + + [n] -> { [i] : exists (a = [i/10] : 0 <= i and i <= n and + i - 10 a <= 6) } + +A set or relation can have several disjuncts, separated +by the keyword C. Each disjunct is either a conjunction +of constraints or a projection (C) of a conjunction +of constraints. The constraints are separated by the keyword +C. + +=head3 C format + +If the represented set is a union, then the first line +contains a single number representing the number of disjuncts. +Otherwise, a line containing the number C<1> is optional. + +Each disjunct is represented by a matrix of constraints. +The first line contains two numbers representing +the number of rows and columns, +where the number of rows is equal to the number of constraints +and the number of columns is equal to two plus the number of variables. +The following lines contain the actual rows of the constraint matrix. +In each row, the first column indicates whether the constraint +is an equality (C<0>) or inequality (C<1>). The final column +corresponds to the constant term. + +If the set is parametric, then the coefficients of the parameters +appear in the last columns before the constant column. +The coefficients of any existentially quantified variables appear +between those of the set variables and those of the parameters. =head3 Input @@ -395,8 +434,8 @@ to foreign file formats. __isl_give isl_map *isl_map_read_from_str(isl_ctx *ctx, const char *str, int nparam); -The input may be either in C format or in the -C format, which is similar to the C format. +The input format is autodetected and may be either the C format +or the C format. C specifies how many of the final columns in the C format correspond to parameters. If input is given in the C format, then the number @@ -423,7 +462,7 @@ are assumed in the C format. void isl_map_print(__isl_keep struct isl_map *map, FILE *out, int indent, unsigned output_format); -C may be either C, C +The C may be either C, C or C. Each line in the output is indented by C spaces, prefixed by C and suffixed by C. @@ -588,6 +627,12 @@ between 10 and 42, you would use the following code. isl_int_clear(v); +Or, alternatively, + + struct isl_basic_set *bset; + bset = isl_basic_set_read_from_str(ctx, + "{[i] : exists (a : i = 2a and i >= 10 and i <= 42)}", -1); + =head2 Properties =head3 Unary Properties @@ -868,20 +913,12 @@ of all elements associated to that element. Although C is mainly meant to be used as a library, it also contains some basic applications that use some of the functionality of C. -Since C does not have its own input format yet, these -applications currently take input in C style. -That is, a line with the number of rows and columns, -where the number of rows is equal to the number of constraints -and the number of columns is equal to two plus the number of variables, -followed by the actual rows. -In each row, the first column indicates whether the constraint -is an equality (C<0>) or inequality (C<1>). The final column -corresponds to the constant term. +The input may specified either in the L +or the L. =head2 C -C -takes a polyhedron in C format as input and prints +C takes a polyhedron as input and prints an integer element of the polyhedron, if there is any. The first column in the output is the denominator and is always equal to 1. If the polyhedron contains no integer points, @@ -891,9 +928,8 @@ then a vector of length zero is printed. C takes the same input as the C program from the C distribution, i.e., a set of constraints -on the parameters in C format, -a line contains only -1 and finally a set -of constraints on a parametric polyhedron, again in C format. +on the parameters, a line contains only -1 and finally a set +of constraints on a parametric polyhedron. The coefficients of the parameters appear in the last columns (but before the final constant column). The output is the lexicographic minimum of the parametric polyhedron. @@ -904,12 +940,12 @@ is just a dump of the internal state. C computes the minimum of some linear or affine objective function over the integer points in a polyhedron. -The input is in C format. If an affine objective function +If an affine objective function is given, then the constant should appear in the last column. =head2 C -Given a polytope in C format, C prints +Given a polytope, C prints all integer points in the polytope. =head1 C -- 2.7.4