next up previous contents
Next: 5.4 Querying variables Up: 5 Querying Existing Relations Previous: 5.2 Printing

5.3 Simplification and satisfiability

A basic function of the library is checking whether a relation is empty (its Presburger formula is unsatisfiable), or whether a relation contains all possible tuples (its Presburger formula is a tautology). Use following member functions to check these conditions.

Figure 5.3 shows some uses of these functions on the sets and relation we built in the previous chapter.

  
Figure 5.1: Example, Part 4: Querying Relations



omega@cs.umd.edu