Safe Haskell	Safe-Infered

Data.Presburger.Omega.LowLevel

Contents

Sets and relations
Inspecting sets and relations directly
Queries on sets and relations
Creating new sets and relations from old ones
Constructing formulas

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

newOmegaSet Source

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

newOmegaRel Source

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

queryDNFSet Source

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.

queryDNFRelation Source

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

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

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

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

definiteTautology :: Presburger a => a -> IO Bool Source

True if the formula is a tautology.

exact :: Presburger a => a -> IO Bool Source

True if the formula has no UNKNOWN constraints.

inexact :: Presburger a => a -> IO Bool Source

True if the formula has UNKNOWN constraints.

unknown :: Presburger a => a -> IO Bool Source

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

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.

composition :: OmegaRel -> OmegaRel -> IO OmegaRel Source

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

restrictDomain :: OmegaRel -> OmegaSet -> IO OmegaRel Source

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

restrictRange :: OmegaRel -> OmegaSet -> IO OmegaRel Source

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.

crossProduct :: OmegaSet -> OmegaSet -> IO OmegaRel Source

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

transitiveClosure :: OmegaRel -> IO OmegaRel Source

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.

domain :: OmegaRel -> IO OmegaSet Source

Get the domain of a relation.

range :: OmegaRel -> IO OmegaSet Source

Get the range of a relation.

inverse :: OmegaRel -> IO OmegaRel Source

Get the inverse of a relation.

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

Get the complement of a set or relation.

deltas :: OmegaRel -> IO OmegaSet Source

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.