Presburger Benchmarks

Operations on Presburger sets have been used for a variety of applications like high-performance computing and machine learning, formal verification, cache modeling, the derivation of data movement bounds, and configurable computing.

Presburger sets are unions of integer polyhedra where some variables can be existentially quantified. A simple example is the set of even numbers ${x : \exists y, y = 2x}$. Although division and modulo constraints are not directly allowed in integer polyhedra, existential quantification allows us to represent operations such as floor division by a constant.

This is a benchmark suite for Presburger arithmetic, operations generated by extracting the Presburger operations performed by the Polly, Pluto, and PPCG compilers when run on Polybench. In particular, the operations extracted are: union, intersect, subtract, complement, coalesce, eliminating existentials, equality checks, and emptiness checks. Eliminating existentials refers to finding a representation of a set containing existentially quantified variables that does not use such quantifiers. This is not always possible; however, for our use case, we additionally allow floor divisions of variables in the output, as these can be handled more easily than arbitrary existentials.

Structure

Each file contains a list of test cases for a particular operation. The first line of the file is the number of test cases, and then each test case follows in succession. Each test case has first the input(s), and then the output given by isl.

• For unary operations complement, coalesce, eliminating existentials, and emptiness checks, the input is one line, containing a single set in isl's input format.
• For binary operations union, intersect, subtract, and equality checks, the input is two lines, each containing a single set in isl's input format.

After the inputs, the output given by isl for the test case is given.

Statistics on the Benchmark

The input sets occurring in the benchmark suite are small and sparse.

• The median number of constraints is zero; and 90% of input sets in the benchmark have at most eight constraints.
• The median dimensionality of the sets is six, and 90% of sets have at most nine dimensions.
• 90% of sets in the input contain only one integer polyhedron.
• 90% of the coefficients in the set constraints are zero, and 99% of coefficients are at most 512.