next up previous
Next: 2 Omega Calculator invocation Up: The Omega Calculator Previous: The Omega Calculator

1 Introduction

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.



next up previous
Next: 2 Omega Calculator invocation Up: The Omega Calculator Previous: The Omega Calculator



omega@cs.umd.edu

Web Accessibility