Safe Haskell | None |
---|
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
- data Set
- set :: Int -> ([Var] -> BoolExp) -> Set
- fromOmegaSet :: OmegaSet -> IO Set
- toOmegaSet :: Set -> OmegaSet
- dimension :: Set -> Int
- predicate :: Set -> BoolExp
- lowerBoundSatisfiable :: Set -> Bool
- upperBoundSatisfiable :: Set -> Bool
- obviousTautology :: Set -> Bool
- definiteTautology :: Set -> Bool
- exact :: Set -> Bool
- inexact :: Set -> Bool
- unknown :: Set -> Bool
- equal :: Set -> Set -> Bool
- upperBound :: Set -> Set
- lowerBound :: Set -> Set
- union :: Set -> Set -> Set
- intersection :: Set -> Set -> Set
- difference :: Set -> Set -> Set
- data Effort
- gist :: Effort -> Set -> Set -> Set
- complement :: Set -> Set
- approximate :: Set -> Set
Documentation
Building sets
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 (\[x,y,z] -> x |>| y |+| z)
Operations on sets
Inspecting
obviousTautology :: Set -> BoolSource
definiteTautology :: Set -> BoolSource
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
upperBound :: Set -> SetSource
Compute the upper bound of a set by setting all UNKNOWN constraints to true.
lowerBound :: Set -> SetSource
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 :: Set -> Set -> SetSource
Intersection of two sets.
The sets must have the same dimension
(dimension s1 == dimension s2
), or an error will be raised.
difference :: Set -> Set -> SetSource
Difference of two sets.
The sets must have the same dimension
(dimension s1 == dimension s2
), or an error will be raised.
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 -> 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
Unary operations
complement :: Set -> SetSource
approximate :: Set -> SetSource