next up previous contents
Next: 2 Compiling And Running Up: 1 Introduction Previous: 1.5 What are uninterpreted

1.6 Manipulating integer tuple relations and sets

A common way to use the library is to build relations and/or sets describing your particular problem, perhaps combine them using the relational operators, and then query them in some way (checking information about a particular variable, checking to see if its formula is satisfiable, or just printing them to the screen.)

In Chapter 4, we describe how to build new relations and sets. In Chapter 5,we describe how to examine existing relations. This includes generating a user readable string representation of a set or relation, and examining the conjuncts and constraints of a relation once it has been simplified and converted into disjunctive normal form (DNF). In Chapter 6, we describe how to create new relations from old relations by applying relational operations such as intersection, union, domain, range, and composition.

In Chapter 2, we discuss some issues related to the compilation of the Omega Library and programs that use it. In Chapter 3, we describe some of the primitive data structures used in the library (such as strings and tuples).