ifscs- An inductive-form set constraint solver

Safe HaskellSafe-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


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


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.


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


data Variance Source

Tags to mark term arguments as covariant or contravariant.



data Inclusion v c Source

An inclusion is a constraint of the form se1 ⊆ se


(Eq v, Eq c) => Eq (Inclusion v c) 
(Ord v, Ord c) => Ord (Inclusion v c) 
(Show v, Show c) => Show (Inclusion v c) 

data SetExpression v c Source

Expressions in the language of set constraints.


(Eq v, Eq c) => Eq (SetExpression v c) 
(Ord v, Ord c) => Ord (SetExpression v c) 
(Show v, Show c) => Show (SetExpression v c) 

data SolvedSystem v c Source

The solved constraint system


(Eq v, Eq c) => Eq (SolvedSystem v c)