Omega-1.0.2: Integer sets and relations using Presburger arithmetic

Safe HaskellNone
LanguageHaskell98

Data.Presburger.Omega.Set

Contents

Description

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

Synopsis

Documentation

data Set Source

Sets of points in Z^n defined by a formula.

Instances

Building sets

set Source

Arguments

:: Int

Number of dimensions

-> ([Var] -> BoolExp)

Predicate defining the set

-> Set 

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)

fromOmegaSet :: OmegaSet -> IO Set Source

Convert an OmegaSet to a Set.

Operations on sets

toOmegaSet :: Set -> OmegaSet Source

Convert a Set to an OmegaSet.

Inspecting

dimension :: Set -> Int Source

Get the dimensionality of the space a set inhabits

predicate :: Set -> BoolExp Source

Get the predicate defining a set's members

exact :: Set -> Bool Source

True if the set has no UNKNOWN constraints.

inexact :: Set -> Bool Source

True if the set has UNKNOWN constraints.

unknown :: Set -> Bool Source

True if the set is completely UNKNOWN.

equal :: Set -> Set -> Bool Source

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 -> Set Source

Compute the upper bound of a set by setting all UNKNOWN constraints to true.

lowerBound :: Set -> Set Source

Compute the lower bound of a set by setting all UNKNOWN constraints to false.

Binary operations

union :: Set -> Set -> Set Source

Union of two sets. The sets must have the same dimension (dimension s1 == dimension s2), or an error will be raised.

intersection :: Set -> Set -> Set Source

Intersection of two sets. The sets must have the same dimension (dimension s1 == dimension s2), or an error will be raised.

difference :: Set -> Set -> Set Source

Difference of two sets. The sets must have the same dimension (dimension s1 == dimension s2), or an error will be raised.

data Effort Source

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 

gist :: Effort -> Set -> Set -> Set Source

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