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) |