Safe Haskell | Safe-Inferred |
---|

This is an implementation of a set (inclusion) constraint solver.

Set constraints, also known as inclusion constraints, are a
convenient, expressive, and efficient way to solve graph
reachability problems. A constraint system consists of set
variables and constructed terms representing atomic literals and
compound terms in the domain. Terms and atomic literals are
*included* in sets by inclusion constraints, and inclusion
relationships are established between set variables.

For example, consider the following constraint system:

5 ⊆ S[B] 6 ⊆ S[B] S[B] ⊆ S[A]

This says that 5 and 6 (atomic literals) are included in the set represented by set variable B. It also says that set B is a subset of set A. Thus, the least solution to this system is:

S[B] = { 5, 6 } S[A] = { 5, 6 }

This example can be solved with this library with the following code:

let constraints = [ atom 6 <=! setVariable "b" , atom 5 <=! setVariable "b" , setVariable "b" <=! setVariable "a" ] Just solved = solveSystem constraints Just solutionA = leastSolution solved "a"

which gives the answer: [ ConstructedTerm 5 [], ConstructedTerm 6
[] ] corresponding to two atoms: 5 and 6. The `solveSystem`

and
`leastSolution`

functions report errors using the `Failure`

abstraction from the failure package. This abstraction lets
callers receive errors in the format they prefer. This example
discards errors by treating them as Maybe values. Errors can be
observed purely using the Either instance of Failure or impurely in
the IO monad using the IO instance.

The implementation is based on the set constraint formulation described in the FFSA98 paper in PLDI'98: http://dx.doi.org/10.1145/277650.277667. Also available at

http://theory.stanford.edu/~aiken/publications/papers/pldi98b.ps

This formulation is notable for representing the constraint graph
in *inductive* form. Briefly, inductive form assigns an ordering
to the set variables in the graph and uses this ordering to reduce
the amount of work required to saturate the graph. The reduction
implies a tradeoff: not all solutions are immediately manifest in
the solved constraint graph. Instead, a DFS is required to extract
each solution.

- emptySet :: SetExpression v c
- universalSet :: SetExpression v c
- setVariable :: Ord v => v -> SetExpression v c
- term :: (Ord v, Ord c) => c -> [Variance] -> [SetExpression v c] -> SetExpression v c
- atom :: Ord c => c -> SetExpression v c
- (<=!) :: (Ord c, Ord v) => SetExpression v c -> SetExpression v c -> Inclusion v c
- solveSystem :: (Failure (ConstraintError v c) m, Eq c, Eq v, Ord c, Ord v) => [Inclusion v c] -> m (SolvedSystem v c)
- leastSolution :: (Failure (ConstraintError v c) m, Ord v, Ord c) => SolvedSystem v c -> v -> m [SetExpression v c]
- data ConstraintError v c
- = NoSolution (Inclusion v c)
- | NoVariableLabel v

- data Variance
- data Inclusion v c
- data SetExpression v c
- = EmptySet
- | UniversalSet
- | SetVariable v
- | ConstructedTerm c [Variance] [SetExpression v c]

- data SolvedSystem v c

# Constructors

emptySet :: SetExpression v cSource

Create a set expression representing the empty set

universalSet :: SetExpression v cSource

Create a set expression representing the universal set

setVariable :: Ord v => v -> SetExpression v cSource

Create a new set variable with the given label

term :: (Ord v, Ord c) => c -> [Variance] -> [SetExpression v c] -> SetExpression v cSource

This returns a function to create terms from lists of SetExpressions. It is meant to be partially applied so that as many terms as possible can share the same reference to a label and signature.

The list of variances specifies the variance (Covariant or Contravariant) for each argument of the term. A mismatch in the length of the variance descriptor and the arguments to the term will result in a run-time error.

atom :: Ord c => c -> SetExpression v cSource

Atomic terms have a label and arity zero. This is a shortcut for

term conLabel [] []

(<=!) :: (Ord c, Ord v) => SetExpression v c -> SetExpression v c -> Inclusion v cSource

Construct an inclusion relation between two set expressions.

This is equivalent to `se1 ⊆ se`

.

# Interface

solveSystem :: (Failure (ConstraintError v c) m, Eq c, Eq v, Ord c, Ord v) => [Inclusion v c] -> m (SolvedSystem v c)Source

Simplify and solve the system of set constraints

leastSolution :: (Failure (ConstraintError v c) m, Ord v, Ord c) => SolvedSystem v c -> v -> m [SetExpression v c]Source

Compute the least solution for the given variable. This can fail
if the requested variable is not present in the constraint system
(see `ConstraintError`

).

LS(y) = All source nodes with a predecessor edge to y, plus LS(x) for all x where x has a predecessor edge to y.

# Types

data ConstraintError v c Source

The types of errors that can be encountered during constraint resolution

NoSolution (Inclusion v c) | The system has no solution because of the given inclusion constraint |

NoVariableLabel v | When searching for a solution, the requested variable was not present in the constraint graph |

Typeable2 ConstraintError | |

(Eq v, Eq c) => Eq (ConstraintError v c) | |

(Ord v, Ord c) => Ord (ConstraintError v c) | |

(Show v, Show c) => Show (ConstraintError v c) | |

(Typeable v, Typeable c, Show v, Show c) => Exception (ConstraintError v c) |

Tags to mark term arguments as covariant or contravariant.

An inclusion is a constraint of the form `se1 ⊆ se`

data SetExpression v c Source

Expressions in the language of set constraints.

EmptySet | |

UniversalSet | |

SetVariable v | |

ConstructedTerm c [Variance] [SetExpression v c] |

(Eq v, Eq c) => Eq (SetExpression v c) | |

(Ord v, Ord c) => Ord (SetExpression v c) | |

(Show v, Show c) => Show (SetExpression v c) |