Boolean operations on semi-linear sets
Supervisor
Suitable for
Abstract
Semi-linear sets are the sets of integers definable in Presburger
arithmetic, the first-order theory of the integers with addition and
order. Their property of being closed under all Boolean operations
makes semi-linear sets a prime choice for finitely representing
infinite sets of integers. The goal of this project is to give an
exposition of algorithms for performing Boolean operations on
semi-linear sets, as well as developing a prototype implementation of
those algorithms and integrating them into the open-source SMT-solver
Z3.