Omega-1.0: Operations on Presburger arithmetic formulae

Data.Presburger.Omega.Set

Description

Sets whose members are represented compactly using a Presburger arithmetic formula. This is a high-level interface to `OmegaSet`.

This module is intended to be imported qualified, e.g.

``` import qualified Data.Presburger.Omega.Set as WSet
```

Synopsis

# Documentation

data Set Source

Sets of points in Z^n defined by a formula.

Instances

 Show Set

# Building sets

Arguments

 :: Int Number of dimensions -> BoolExp Predicate defining the set -> Set

Create a set whose members are defined by a predicate.

The expression should have one free variable for each dimension.

For example, the set of all points on the plane is

```  set 2 trueE
```

The set of all points (x, y, z) where x > y + z is

```  set 3 (case takeFreeVariables' 3 of [x,y,z] -> x |>| y |+| z)
```

Convert an `OmegaSet` to a `Set`.

# Operations on sets

Convert a `Set` to an `OmegaSet`.

## Inspecting

Get the dimensionality of the space a set inhabits

Get the predicate defining a set's members

True if the set has no UNKNOWN constraints.

True if the set has UNKNOWN constraints.

True if the set is completely UNKNOWN.

equal :: Set -> Set -> BoolSource

Test whether two sets are equal. The sets must have the same dimension (`dimension s1 == dimension s2`), or an error will be raised.

The answer is precise if both relations are `exact`. If either relation is inexact, this function returns `False`.

## Bounds

Compute the upper bound of a set by setting all UNKNOWN constraints to true.

Compute the lower bound of a set by setting all UNKNOWN constraints to false.

## Binary operations

union :: Set -> Set -> SetSource

Union of two sets. The sets must have the same dimension (`dimension s1 == dimension s2`), or an error will be raised.

Intersection of two sets. The sets must have the same dimension (`dimension s1 == dimension s2`), or an error will be raised.

Difference of two sets. The sets must have the same dimension (`dimension s1 == dimension s2`), or an error will be raised.

data Effort Source

The `gist` routine takes a parameter specifying how much effort to put into generating a good result. Higher effort takes more time. It's unspecified what a given effort level does.

Constructors

 Light Moderate Strenuous

Instances

 Enum Effort Eq Effort Show Effort

gist :: Effort -> Set -> Set -> SetSource

Get the gist of a set, given some background truth. The gist operator uses heuristics to simplify the set while retaining sufficient information to regenerate the original by re-introducing the background truth. The sets must have the same dimension.

The gist satisfies the property

``` x === gist effort x given `intersection` given
```