Safe Haskell | None |
---|---|
Language | Haskell98 |
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.
- class Presburger a
- data OmegaSet
- newOmegaSet :: Int -> ([VarHandle] -> Formula) -> IO OmegaSet
- data OmegaRel
- newOmegaRel :: Int -> Int -> ([VarHandle] -> [VarHandle] -> Formula) -> IO OmegaRel
- queryDNFSet :: ([VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> a -> a) -> a -> ([VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> b -> b) -> b -> ([VarHandle] -> [VarHandle] -> a -> b -> c -> c) -> c -> OmegaSet -> IO ([VarHandle], c)
- queryDNFRelation :: ([VarHandle] -> [VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> a -> a) -> a -> ([VarHandle] -> [VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> b -> b) -> b -> ([VarHandle] -> [VarHandle] -> [VarHandle] -> a -> b -> c -> c) -> c -> OmegaRel -> IO ([VarHandle], [VarHandle], c)
- lowerBoundSatisfiable :: Presburger a => a -> IO Bool
- upperBoundSatisfiable :: Presburger a => a -> IO Bool
- obviousTautology :: Presburger a => a -> IO Bool
- definiteTautology :: Presburger a => a -> IO Bool
- exact :: Presburger a => a -> IO Bool
- inexact :: Presburger a => a -> IO Bool
- unknown :: Presburger a => a -> IO Bool
- upperBound :: Presburger a => a -> IO a
- lowerBound :: Presburger a => a -> IO a
- equal :: Presburger a => a -> a -> IO Bool
- union :: Presburger a => a -> a -> IO a
- intersection :: Presburger a => a -> a -> IO a
- composition :: OmegaRel -> OmegaRel -> IO OmegaRel
- restrictDomain :: OmegaRel -> OmegaSet -> IO OmegaRel
- restrictRange :: OmegaRel -> OmegaSet -> IO OmegaRel
- difference :: Presburger a => a -> a -> IO a
- crossProduct :: OmegaSet -> OmegaSet -> IO OmegaRel
- data Effort
- gist :: Presburger a => Effort -> a -> a -> IO a
- transitiveClosure :: OmegaRel -> IO OmegaRel
- domain :: OmegaRel -> IO OmegaSet
- range :: OmegaRel -> IO OmegaSet
- inverse :: OmegaRel -> IO OmegaRel
- complement :: Presburger a => a -> IO a
- deltas :: OmegaRel -> IO OmegaSet
- approximate :: Presburger a => a -> IO a
- data Formula
- true :: Formula
- false :: Formula
- conjunction :: [Formula] -> Formula
- disjunction :: [Formula] -> Formula
- negation :: Formula -> Formula
- data VarHandle
- qForall :: (VarHandle -> Formula) -> Formula
- qExists :: (VarHandle -> Formula) -> Formula
- data Coefficient = Coefficient {
- coeffVar :: !VarHandle
- coeffValue :: !Int
- inequality :: [Coefficient] -> Int -> Formula
- equality :: [Coefficient] -> Int -> Formula
Sets and relations
A set of points in Z^n. This is a wrapper around the Omega library's Relation type.
:: 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.
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.
:: 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
:: ([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.
:: ([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 a Source
Compute the upper bound of a set or relation by setting all UNKNOWN constraints to true.
lowerBound :: Presburger a => a -> IO a Source
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 a Source
Compute the union of two sets or relations. The sets or relations must have the same arity.
intersection :: Presburger a => a -> a -> IO a Source
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 a Source
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
.
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 :: Presburger a => Effort -> a -> a -> IO a Source
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.
complement :: Presburger a => a -> IO a Source
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 a Source
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
conjunction :: [Formula] -> Formula Source
Logical conjunction (and).
disjunction :: [Formula] -> Formula Source
Logical disjunction (or).
qForall :: (VarHandle -> Formula) -> Formula Source
Universal quantification. The VarHandle
parameter is the variable
bound by the quantifier.
qExists :: (VarHandle -> Formula) -> Formula Source
Existential quantification. The VarHandle
parameter is the variable
bound by the quantifier.
data Coefficient Source
An integer-valued term n*v
in a formula.
Coefficient | |
|
inequality :: [Coefficient] -> Int -> Formula Source
Construct an inequation of the form a*x + b*y + ... + d >= 0
.
equality :: [Coefficient] -> Int -> Formula Source
Construct an equation of the form a*x + b*y + ... + d = 0
.