Omega-1.0.3: Integer sets and relations using Presburger arithmetic

Data.Presburger.Omega.Rel

Description

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

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

``` import qualified Data.Presburger.Omega.Rel as WRel
```

Synopsis

# Documentation

data Rel Source

A relation from points in a domain Z^m to points in a range Z^n.

A relation can be considered just a set of points in Z^(m+n). However, many functions that operate on relations treat the domain and range differently.

Instances

 Show Rel

# Building relations

Arguments

 :: Int Dimensionality of the domain -> Int Dimensionality of the range -> BoolExp Predicate defining the relation -> Rel

Create a relation whose members are defined by a predicate.

The expression should have `m+n` free variables, where `m` and `n` are the first two parameters. The first `m` variables refer to the domain, and the remaining variables refer to the range.

Arguments

 :: Int Dimensionality of the domain -> [IntExp] Function relating domain to range -> BoolExp Predicate restricting the domain -> Rel

Create a relation where each output is a function of the inputs.

Each expression should have `m` free variables, where `m` is the first parameter.

For example, the relation `{(x, y) -> (y, x) | x > 0 && y > 0}` is

``` let [x, y] = takeFreeVariables' 2
in functionalRel 2 [y, x] (conjE [y |>| intE 0, x |>| intE 0])
```

Convert an `OmegaRel` to a `Rel`.

# Operations on relations

Convert a `Rel` to an `OmegaRel`.

## Inspecting

Get the dimensionality of a relation's domain

Get the dimensionality of a relation's range

Get the predicate defining a relation.

True if the relation has no UNKNOWN constraints.

True if the relation has UNKNOWN constraints.

True if the relation is entirely UNKNOWN.

equal :: Rel -> Rel -> BoolSource

Test whether two relations are equal. The relations must have the same dimension (`inputDimension r1 == inputDimension r2 && outputDimension r1 == outputDimension r2`), or an error will be raised.

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

## Binary operations

union :: Rel -> Rel -> RelSource

Union of two relations. The relations must have the same dimension (`inputDimension r1 == inputDimension r2 && outputDimension r1 == outputDimension r2`), or an error will be raised.

Intersection of two relations. The relations must have the same dimension (`inputDimension r1 == inputDimension r2 && outputDimension r1 == outputDimension r2`), or an error will be raised.

Composition of two relations. The second relation's output must be the same size as the first's input (`outputDimension r2 == inputDimension r1`), or an error will be raised.

join :: Rel -> Rel -> RelSource

Same as `composition`, with the arguments swapped.

Restrict the domain of a relation.

``` domain (restrictDomain r s) === intersection (domain r) s
```

Restrict the range of a relation.

``` range (restrictRange r s) === intersection (range r) s
```

Difference of two relations. The relations must have the same dimension (`inputDimension r1 == inputDimension r2 && outputDimension r1 == outputDimension r2`), or an error will be raised.

Cross product of two sets.

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 -> Rel -> Rel -> RelSource

Get the gist of a relation, given some background truth. The gist operator uses heuristics to simplify the relation while retaining sufficient information to regenerate the original by re-introducing the background truth. The relations must have the same input dimensions and the same output dimensions.

The gist satisfies the property

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

## Unary operations

Get the transitive closure of a relation. In some cases, the transitive closure cannot be computed exactly, in which case a lower bound is returned.

Invert a relation, swapping the domain and range.

Get the complement of a relation.

Approximate a relation by allowing all existentially quantified variables to take on rational values. This allows these variables to be eliminated from the formula.