Safe Haskell | None |
---|

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

- data Rel
- rel :: Int -> Int -> BoolExp -> Rel
- functionalRel :: Int -> [IntExp] -> BoolExp -> Rel
- fromOmegaRel :: OmegaRel -> IO Rel
- toOmegaRel :: Rel -> OmegaRel
- inputDimension :: Rel -> Int
- outputDimension :: Rel -> Int
- predicate :: Rel -> BoolExp
- lowerBoundSatisfiable :: Rel -> Bool
- upperBoundSatisfiable :: Rel -> Bool
- obviousTautology :: Rel -> Bool
- definiteTautology :: Rel -> Bool
- exact :: Rel -> Bool
- inexact :: Rel -> Bool
- unknown :: Rel -> Bool
- equal :: Rel -> Rel -> Bool
- upperBound :: Rel -> Rel
- lowerBound :: Rel -> Rel
- union :: Rel -> Rel -> Rel
- intersection :: Rel -> Rel -> Rel
- composition :: Rel -> Rel -> Rel
- join :: Rel -> Rel -> Rel
- restrictDomain :: Rel -> Set -> Rel
- restrictRange :: Rel -> Set -> Rel
- difference :: Rel -> Rel -> Rel
- crossProduct :: Set -> Set -> Rel
- data Effort
- gist :: Effort -> Rel -> Rel -> Rel
- transitiveClosure :: Rel -> Rel
- domain :: Rel -> Set
- range :: Rel -> Set
- inverse :: Rel -> Rel
- complement :: Rel -> Rel
- deltas :: Rel -> Set
- approximate :: Rel -> Rel

# Documentation

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.

# Building relations

:: 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.

:: 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])

# Operations on relations

## Inspecting

inputDimension :: Rel -> IntSource

Get the dimensionality of a relation's domain

outputDimension :: Rel -> IntSource

Get the dimensionality of a relation's range

obviousTautology :: Rel -> BoolSource

definiteTautology :: Rel -> BoolSource

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`

.

## Bounds

upperBound :: Rel -> RelSource

lowerBound :: Rel -> RelSource

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

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

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.

restrictDomain :: Rel -> Set -> RelSource

Restrict the domain of a relation.

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

restrictRange :: Rel -> Set -> RelSource

Restrict the range of a relation.

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

difference :: Rel -> Rel -> RelSource

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.

crossProduct :: Set -> Set -> RelSource

Cross product of two sets.

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.

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

transitiveClosure :: Rel -> RelSource

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.

complement :: Rel -> RelSource

Get the complement of a relation.

approximate :: Rel -> RelSource

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