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