Data.Presburger.Omega.Rel

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

Documentation

data Rel

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

rel

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.

functionalRel

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

fromOmegaRel :: OmegaRel -> IO Rel

Convert an OmegaRel to a Rel.

Operations on relations

toOmegaRel :: Rel -> OmegaRel

Convert a Rel to an OmegaRel.

Inspecting

inputDimension :: Rel -> Int

Get the dimensionality of a relation's domain

outputDimension :: Rel -> Int

Get the dimensionality of a relation's range

predicate :: Rel -> BoolExp

Get the predicate defining a relation.

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

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

lowerBound :: Rel -> Rel

Binary operations

union :: Rel -> Rel -> Rel

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

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

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

Same as composition, with the arguments swapped.

restrictDomain :: Rel -> Set -> Rel

restrictRange :: Rel -> Set -> Rel

difference :: Rel -> Rel -> Rel

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

Cross product of two sets.

data Effort

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

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

domain :: Rel -> Set

range :: Rel -> Set

inverse :: Rel -> Rel

complement :: Rel -> Rel

deltas :: Rel -> Set

approximate :: Rel -> Rel