Omega-1.0: Operations on Presburger arithmetic formulae

Safe Haskell Safe-Infered

Data.Presburger.Omega.LowLevel

Description

This module provides a low-level interface for creating, manipulating, and querying Presburger arithmetic formulae. The real work is done by the C++ Omega library (http://github.com/davewathaverford/the-omega-project).

The main data types are `OmegaSet` and `OmegaRel`, which use a formula to define a set or relation, respectively, on integer-valued points in Cartesian space. A typical use involves creating a Presburger arithmetic `Formula`, using it to create a set or relation, and then querying the set or relation.

Synopsis

# Sets and relations

class Presburger a Source

Data types containing Presburger formulae.

Instances

 Presburger OmegaRel Presburger OmegaSet

data OmegaSet Source

A set of points in Z^n. This is a wrapper around the Omega library's Relation type.

Instances

 Show OmegaSet Presburger OmegaSet

Arguments

 :: Int Dimensionality of the space that the set inhabits -> ([VarHandle] -> Formula) Set members -> IO OmegaSet

Create an Omega set. The first parameter is the number of dimensions the set inhabits. The second parameter builds a formula defining the set's members. The set's members are those points for which the formula evaluates to True.

data OmegaRel Source

A relation from points in a domain Z^m to points in a range Z^n. This is a wrapper around the Omega library's Relation type.

A relation can be considered as just a set of points in Z^(m+n). However, many routines treat the domain and range differently.

Instances

 Show OmegaRel Presburger OmegaRel

Arguments

 :: Int Dimensionality of the domain -> Int Dimensionality of the range -> ([VarHandle] -> [VarHandle] -> Formula) The relation -> IO OmegaRel

Create an Omega relation. The first two parameters are the number of dimensions of the domain and range, respectively. The third parameter builds a formula defining the relation. Two points are related iff the formula evaluates to True on those points.

# Inspecting sets and relations directly

Arguments

 :: ([VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> a -> a) Accumulating function for equality constraints -> a Initial value for equality constraints -> ([VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> b -> b) Accumulating function for inequality constraints -> b Initial value for inequality constraints -> ([VarHandle] -> [VarHandle] -> a -> b -> c -> c) Accumulating function for conjuncts -> c Initial value for conjuncts -> OmegaSet Set to query -> IO ([VarHandle], c)

Inspect a set's low-level representation directly. This function takes care of data structure traversal and relies on other routines to interpret the data.

All three accumulating functions take the set variables as their first parameter, and any existentially quantified variables as their second parameter. The set variables are returned along with a result value.

Arguments

 :: ([VarHandle] -> [VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> a -> a) Accumulating function for equality constraints -> a Initial value for equality constraints -> ([VarHandle] -> [VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> b -> b) Accumulating function for inequality constraints -> b Initial value for inequality constraints -> ([VarHandle] -> [VarHandle] -> [VarHandle] -> a -> b -> c -> c) Accumulating function for conjuncts -> c Initial value for conjuncts -> OmegaRel Relation to query -> IO ([VarHandle], [VarHandle], c) Input variables, output variables, and result

Inspect a relation's low-level representation directly. This function takes care of data structure traversal and relies on other routines to interpret the data.

All three accumulating functions take the relation's input and output variables as their first and second parameters, respectively, and any existentially quantified variables as their second parameter. The relation's input and output variables are returned along with a result value.

# Queries on sets and relations

lowerBoundSatisfiable :: Presburger a => a -> IO BoolSource

Determine a lower bound on whether the formula is satisfiable. The lower bound is based on treating all UNKNOWN constraints as false.

upperBoundSatisfiable :: Presburger a => a -> IO BoolSource

Determine an upper bound on whether the formula is satisfiable. The upper bound is based on treating all UNKNOWN constraints as true.

obviousTautology :: Presburger a => a -> IO BoolSource

Use simple, fast tests to decide whether the formula is a tautology.

definiteTautology :: Presburger a => a -> IO BoolSource

True if the formula is a tautology.

exact :: Presburger a => a -> IO BoolSource

True if the formula has no UNKNOWN constraints.

inexact :: Presburger a => a -> IO BoolSource

True if the formula has UNKNOWN constraints.

unknown :: Presburger a => a -> IO BoolSource

True if the formula is UNKNOWN.

# Creating new sets and relations from old ones

## Bounds

upperBound :: Presburger a => a -> IO aSource

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

lowerBound :: Presburger a => a -> IO aSource

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

## Binary operations

equal :: Presburger a => a -> a -> IO BoolSource

Test whether two sets or relations are equal. The sets or relations must have the same arity.

The answer is precise if both arguments are `exact`. If either argument is inexact, this function returns `False`.

union :: Presburger a => a -> a -> IO aSource

Compute the union of two sets or relations. The sets or relations must have the same arity.

intersection :: Presburger a => a -> a -> IO aSource

Compute the intersection of two sets or relations. The sets or relations must have the same arity.

Compute the composition of two sets or relations. The first relation's domain must be the same dimension as the second's range.

Restrict the domain of a relation. If `domain r` is `d`, then `domain =<< restrictDomain r s` is `intersection d s`.

Restrict the range of a relation. If `range r` is `d`, then `range =<< restrictRange r s` is `intersection d s`.

difference :: Presburger a => a -> a -> IO aSource

Compute the difference of two relations or sets. The members of `difference x y` are the members of `x` that are not members of `y`.

Compute the cross product of two sets. The cross product relates every element of `s` to every element of `y`.

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

Instances

 Enum Effort Eq Effort Show Effort

gist :: Presburger a => Effort -> a -> a -> IO aSource

Get the gist of a set or relation, given some background truth. The gist operator uses heuristics to make a set or relation simpler, while still retaining sufficient information to regenerate the original by re-introducing the background truth. The sets or relations must have the same arity.

Given `x` computed by

``` x <- intersection given =<< gist effort r given
```

we have `x == r`.

## Unary operations

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.

Get the domain of a relation.

Get the range of a relation.

Get the inverse of a relation.

complement :: Presburger a => a -> IO aSource

Get the complement of a set or relation.

Get the deltas of a relation. The relation's input dimensionality must be the same as its output dimensionality.

approximate :: Presburger a => a -> IO aSource

Approximate a set or relation by allowing all existentially quantified variables to take on rational values. This allows these variables to be eliminated from the formula.

# Constructing formulas

data Formula Source

A boolean-valued Presburger formula.

Truth.

Falsity.

conjunction :: [Formula] -> FormulaSource

Logical conjunction (and).

disjunction :: [Formula] -> FormulaSource

Logical disjunction (or).

Logical negation.

data VarHandle Source

A variable in a formula.

Instances

 Eq VarHandle

qForall :: (VarHandle -> Formula) -> FormulaSource

Universal quantification. The `VarHandle` parameter is the variable bound by the quantifier.

qExists :: (VarHandle -> Formula) -> FormulaSource

Existential quantification. The `VarHandle` parameter is the variable bound by the quantifier.

An integer-valued term `n*v` in a formula.

Constructors

 Coefficient FieldscoeffVar :: !VarHandle coeffValue :: !Int

Instances

 Show Coefficient Storable Coefficient

inequality :: [Coefficient] -> Int -> FormulaSource

Construct an inequation of the form `a*x + b*y + ... + d >= 0`.

equality :: [Coefficient] -> Int -> FormulaSource

Construct an equation of the form `a*x + b*y + ... + d = 0`.