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.