This document gives an overview of the Omega library and describes the Omega Calculator, a text-based interface to the Omega library. A separate document describes the C++ interface to the Omega library and we are still working on a third document that describes some of the algorithms used in implementing the Omega library.
The Omega library manipulates integer tuple relations and sets, such as
Tuple relations and
sets are described using Presburger
formulas[KK67,Sho77,Coo72,Coo71] a class of logical
formulas which can be built from affine constraints over integer
variables, the logical connectives 
, 
and 
, and the
quantifiers 
and 
.
The best known upper bound on the performance of an algorithm for
verifying Presburger formulas is 
[Opp78],
and we have no
reason to believe that our method provides better worst-case
performance. However, we have found it
to be reasonably efficient for our applications.
The following relation, which maps 2-tuples to 1-tuples:
represents the following set of mappings: 
.
In addition to variables in the input and output tuples, the Presburger
formulas may also contain free variables. This allows parameterized relations to be described.
For example, n and m are free in
.
The language allows new relations to be defined in terms of existing relations
by providing a number of relational operators. The relational operations
provided include intersection, union, composition, inverse, domain, range and complement.
For example, 
compose
evaluates to
.
Relations are simplified before being displayed to the user. This
involves transforming them into disjunctive normal form and removing
redundant constraints and conjuncts. During simplification, it may be determined
that the relation contains no points or contains all points, in which
case the simplified constraints will be False or True respectively.
For example, 
intersect
evaluates to 
.
The copyright notice and legal fine print for the Omega calculator and library are contained in the README and omega.h files. Basically, you can do anything you want with them (other than sue us); if you redistribute it you must include a copy of our copyright notice and legal fine print.