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.