diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2012, Tristan Ravitch
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Tristan Ravitch nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/ifscs.cabal b/ifscs.cabal
new file mode 100644
--- /dev/null
+++ b/ifscs.cabal
@@ -0,0 +1,35 @@
+name:                ifscs
+version:             0.2.0.0
+synopsis:            An inductive-form set constraint solver
+license:             BSD3
+license-file:        LICENSE
+author:              Tristan Ravitch
+maintainer:          travitch@cs.wisc.edu
+category:            Constraints
+build-type:          Simple
+cabal-version:       >=1.10
+description: This is an implementation of an (inclusion) set constraint
+             solver.  Set constraints are a convenient and efficient way
+             to specify and solve graph reachability problems.
+             .
+             See the Constraints.Set.Solver module for detailed documentation.
+
+library
+  default-language: Haskell2010
+  exposed-modules: Constraints.Set.Solver
+  other-modules: Constraints.Set.Implementation
+  build-depends: base == 4.*,
+                 failure >= 0.2 && < 0.3,
+                 containers
+  hs-source-dirs: src
+  ghc-options: -Wall
+  ghc-prof-options: -auto-all
+
+test-suite ConstraintTests
+  default-language: Haskell2010
+  type: exitcode-stdio-1.0
+  hs-source-dirs: tests
+  main-is: ConstraintTests.hs
+  build-depends: ifscs, base,
+                 test-framework, test-framework-hunit, HUnit
+  ghc-options: -Wall -threaded
diff --git a/src/Constraints/Set/Implementation.hs b/src/Constraints/Set/Implementation.hs
new file mode 100644
--- /dev/null
+++ b/src/Constraints/Set/Implementation.hs
@@ -0,0 +1,453 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE BangPatterns #-}
+module Constraints.Set.Implementation (
+  ConstraintError(..),
+  Variance(..),
+  Inclusion,
+  SetExpression(..),
+  SolvedSystem,
+  emptySet,
+  universalSet,
+  setVariable,
+  atom,
+  term,
+  (<=!),
+  solveSystem,
+  leastSolution
+  ) where
+
+import Control.Exception
+import Control.Failure
+import qualified Data.Foldable as F
+import Data.Function ( on )
+import qualified Data.List as L
+import Data.Map ( Map )
+import qualified Data.Map as M
+import Data.Maybe ( fromMaybe )
+import Data.Monoid
+import Data.Set ( Set )
+import qualified Data.Set as S
+import Data.Typeable
+
+type Worklist v c = Set (PredSegment v c)
+
+-- | The type used to represent that inductive form constraint graph
+-- during saturation.  This form is more efficient to saturate.
+type IFGraph v c = Map (SetExpression v c) (Edges v c)
+
+data Edges v c = Edges { predecessors :: Set (SetExpression v c)
+                       , successors :: Set (SetExpression v c)
+                       }
+               deriving (Eq, Ord)
+
+-- | The solved constraint system
+data SolvedSystem v c =
+  SolvedSystem { systemIFGraph :: IFGraph v c  }
+
+instance (Eq v, Eq c) => Eq (SolvedSystem v c) where
+  (==) = (==) `on` systemIFGraph
+
+
+-- | A type describing an edge added in one iteration of the
+-- transitive closure.  These let us know which nodes need to be
+-- revisited in the next iteration (and in which direction -
+-- predecessor or successor)
+data PredSegment v c = PSPred (SetExpression v c) (SetExpression v c)
+                     | PSSucc (SetExpression v c) (SetExpression v c)
+                     deriving (Eq, Ord)
+
+-- | Create a set expression representing the empty set
+emptySet :: SetExpression v c
+emptySet = EmptySet
+
+-- | Create a set expression representing the universal set
+universalSet :: SetExpression v c
+universalSet = UniversalSet
+
+-- | Create a new set variable with the given label
+setVariable :: (Ord v) => v -> SetExpression v c
+setVariable = SetVariable
+
+-- | Atomic terms have a label and arity zero.  This is a shortcut for
+--
+-- > term conLabel [] []
+atom :: (Ord c) => c -> SetExpression v c
+atom conLabel = ConstructedTerm conLabel [] []
+
+-- | 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.
+term :: (Ord v, Ord c) => c -> [Variance] -> ([SetExpression v c] -> SetExpression v c)
+term = ConstructedTerm
+
+-- | Construct an inclusion relation between two set expressions.
+--
+-- This is equivalent to @se1 ⊆ se2@.
+(<=!) :: (Ord c, Ord v) => SetExpression v c -> SetExpression v c -> Inclusion v c
+(<=!) = Inclusion
+
+-- | Tags to mark term arguments as covariant or contravariant.
+data Variance = Covariant | Contravariant
+              deriving (Eq, Ord, Show)
+
+-- | Expressions in the language of set constraints.
+data SetExpression v c = EmptySet
+                       | UniversalSet
+                       | SetVariable v
+                       | ConstructedTerm c [Variance] [SetExpression v c]
+                       deriving (Eq, Ord)
+
+instance (Show v, Show c) => Show (SetExpression v c) where
+  show EmptySet = "∅"
+  show UniversalSet = "U"
+  show (SetVariable v) = show v
+  show (ConstructedTerm c _ es) =
+    concat [ show c, "("
+           , L.intercalate ", " (map show es)
+           , ")"
+           ]
+
+-- | An inclusion is a constraint of the form @se1 ⊆ se2@
+data Inclusion v c =
+  Inclusion (SetExpression v c) (SetExpression v c)
+  deriving (Eq, Ord)
+
+
+
+instance (Show v, Show c) => Show (Inclusion v c) where
+  show (Inclusion lhs rhs) = concat [ show lhs, " ⊆ ", show rhs ]
+
+-- | The types of errors that can be encountered during constraint
+-- resolution
+data ConstraintError v c = 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
+                         deriving (Eq, Ord, Show, Typeable)
+
+instance (Typeable v, Typeable c, Show v, Show c) => Exception (ConstraintError v c)
+
+-- | Simplify one set expression.  The expression may be eliminated,
+-- passed through unchanged, or split into multiple new expressions.
+simplifyInclusion :: (Ord c, Ord v, Eq v, Eq c)
+                     => Inclusion v c -- ^ The inclusion to be simplified
+                     -> [Inclusion v c]
+simplifyInclusion i =
+  case i of
+    -- Eliminate constraints of the form A ⊆ A
+    Inclusion (SetVariable v1) (SetVariable v2) ->
+      if v1 == v2 then [] else [i]
+    Inclusion UniversalSet EmptySet ->
+      error "Malformed constraint univ < emptyset"
+    Inclusion (ConstructedTerm c1 s1 ses1) (ConstructedTerm c2 s2 ses2) ->
+      let sigLen = length s1
+          triples = zip3 s1 ses1 ses2
+      in case c1 == c2 && s1 == s2 && sigLen == length ses1 && sigLen == length ses2 of
+        False -> error "Malformed constraint cterm mismatch"
+        True -> concatMap simplifyWithVariance triples
+    Inclusion UniversalSet (ConstructedTerm _ _ _) ->
+      error "Malformed constraint univ < cterm"
+    Inclusion (ConstructedTerm _ _ _) EmptySet ->
+      error "Malformed constraint cterm < emptyset"
+    -- Eliminate constraints of the form A ⊆ 1
+    Inclusion _ UniversalSet -> []
+    -- 0 ⊆ A
+    Inclusion EmptySet _ -> []
+    -- Keep anything else (atomic forms)
+    _ -> [i]
+
+-- | Simplifies an inclusion taking variance into account; this is a
+-- helper for 'simplifyInclusion' that deals with the variance of
+-- constructed terms.  The key here is that contravariant inclusions
+-- are /flipped/.
+simplifyWithVariance :: (Ord c, Ord v, Eq v, Eq c)
+                        => (Variance, SetExpression v c, SetExpression v c)
+                        -> [Inclusion v c]
+simplifyWithVariance (Covariant, se1, se2) =
+  simplifyInclusion (Inclusion se1 se2)
+simplifyWithVariance (Contravariant, se1, se2) =
+  simplifyInclusion (Inclusion se2 se1)
+
+-- | Simplify all of the inclusions in the initial constraint system.
+simplifySystem :: (Ord c, Ord v, Eq v, Eq c)
+                  => [Inclusion v c]
+                  -> [Inclusion v c]
+simplifySystem = concatMap simplifyInclusion
+
+dfs :: (Ord c, Ord v) => IFGraph v c -> SetExpression v c -> Set (SetExpression v c)
+dfs g = go mempty
+  where
+    go !visited v =
+      case M.lookup v g of
+        Nothing -> visited
+        Just Edges { predecessors = ps } ->
+          F.foldl' go (S.union ps visited) ps
+
+-- | 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.
+leastSolution :: (Failure (ConstraintError v c) m, Ord v, Ord c)
+                 => SolvedSystem v c
+                 -> v
+                 -> m [SetExpression v c]
+leastSolution (SolvedSystem g0) varLabel = do
+  let reached = dfs g0 (SetVariable varLabel)
+  return $ F.foldr addTerm [] reached
+  where
+    -- ex :: ConstraintError v c
+    -- ex = NoVariableLabel varLabel
+
+    addTerm v acc =
+      case v of
+        ConstructedTerm _ _ _ -> v : acc
+        _ -> acc
+
+-- | Simplify and solve the system of set constraints
+solveSystem :: (Failure (ConstraintError v c) m, Eq c, Eq v, Ord c, Ord v)
+               => [Inclusion v c]
+               -> m (SolvedSystem v c)
+solveSystem = return . constraintsToIFGraph . simplifySystem
+
+-- | The real worker to solve the system and convert from an IFGraph
+-- to a SolvedGraph.
+constraintsToIFGraph :: (Ord v, Ord c) => [Inclusion v c] -> SolvedSystem v c
+constraintsToIFGraph is =
+  SolvedSystem { systemIFGraph = saturateGraph g0 wl }
+  where
+    (g0, wl) = buildInitialGraph is
+
+-- | Build an initial IF constraint graph that contains all of the
+-- vertices and the edges induced by the initial simplified constraint
+-- system.
+buildInitialGraph :: (Ord v, Ord c)
+                     => [Inclusion v c]
+                     -> (IFGraph v c, Worklist v c)
+buildInitialGraph is = L.foldl' addInclusion (mempty, mempty) is
+
+-- | Adds an inclusion to the constraint graph (adding vertices if
+-- necessary).  Returns the set of nodes that are affected (and will
+-- need more transitive edges).
+addInclusion :: (Eq c, Ord v, Ord c)
+                => (IFGraph v c, Worklist v c)
+                -> Inclusion v c
+                -> (IFGraph v c, Worklist v c)
+addInclusion acc i =
+  case i of
+    -- This is the key to an inductive form graph (rather than
+    -- standard form)
+    Inclusion e1@(SetVariable v1) e2@(SetVariable v2)
+      | v1 < v2 -> addSuccEdge acc e1 e2
+      | otherwise -> addPredEdge acc e1 e2
+    Inclusion e1@(ConstructedTerm _ _ _) e2@(SetVariable _) ->
+      addPredEdge acc e1 e2
+    Inclusion e1@(SetVariable _) e2@(ConstructedTerm _ _ _) ->
+      addSuccEdge acc e1 e2
+    _ -> error "Constraints.Set.Solver.addInclusion: unexpected expression"
+
+-- | Add a predecessor edge (l is a predecessor of r)
+addPredEdge :: (Ord c, Ord v)
+               => (IFGraph v c, Worklist v c)
+               -> SetExpression v c
+               -> SetExpression v c
+               -> (IFGraph v c, Worklist v c)
+addPredEdge acc@(!g, !work) l r =
+  case M.lookup r g of
+    Nothing ->
+      let es = Edges { predecessors = S.singleton l, successors = S.empty }
+      in (M.insert r es g, S.insert (PSPred l r) work)
+    Just es
+      | S.member l (predecessors es) -> acc
+      | otherwise ->
+        let es' = es { predecessors = S.insert l (predecessors es) }
+        in (M.insert r es' g, S.insert (PSPred l r) work)
+
+addSuccEdge :: (Ord c, Ord v)
+               => (IFGraph v c, Worklist v c)
+               -> SetExpression v c
+               -> SetExpression v c
+               -> (IFGraph v c, Worklist v c)
+addSuccEdge acc@(!g, !work) l r =
+  case M.lookup l g of
+    Nothing ->
+      let es = Edges { predecessors = S.empty, successors = S.singleton r }
+      in (M.insert l es g, S.insert (PSSucc l r) work)
+    Just es
+      | S.member r (successors es) -> acc
+      | otherwise ->
+        let es' = es { successors = S.insert r (successors es) }
+        in (M.insert l es' g, S.insert (PSSucc l r) work)
+
+-- | For each node L in the graph, follow its predecessor edges to
+-- obtain set X.  For each ndoe in X, follow its successor edges
+-- giving a list of R.  Generate L ⊆ R and simplify it with
+-- 'simplifyInclusion'.  These are new edges (collect them all in a
+-- set, discarding existing edges).
+--
+-- After a pass, insert all of the new edges
+--
+-- Repeat until no new edges are found.
+--
+-- An easy optimization is to base the next iteration only on the
+-- newly-added edges (since any additions in the next iteration must
+-- be due to those new edges).  It would require searching forward
+-- (for pred edges) and backward (for succ edges).
+--
+-- Also perform online cycle detection per FFSA98
+--
+-- This function can fail if a constraint generated by the saturation
+-- implies that no solution is possible.  I think that probably
+-- shouldn't ever happen but I have no proof.
+saturateGraph :: (Ord v, Ord c, Eq c)
+                 => IFGraph v c
+                 -> Worklist v c
+                 -> IFGraph v c
+saturateGraph g0 wl0 =
+  let (g1, wl1) = F.foldl' addNewEdges (g0, mempty) wl0
+  in if S.null wl1 then g1 else saturateGraph g1 wl1
+
+addNewEdges :: (Ord v, Ord c)
+               => (IFGraph v c, Worklist v c)
+               -> PredSegment v c
+               -> (IFGraph v c, Worklist v c)
+addNewEdges acc@(!g0, _) (PSPred l r) = fromMaybe acc $ do
+  Edges { successors = ss } <- M.lookup r g0
+  return $ F.foldl' (addNewInclusions l) acc ss
+  where
+    addNewInclusions lhs a rhs =
+      F.foldl' addInclusion a $ simplifyInclusion (Inclusion lhs rhs)
+addNewEdges acc@(!g0, _) (PSSucc l r) = fromMaybe acc $ do
+  Edges { predecessors = ps } <- M.lookup l g0
+  return $ F.foldl' (addNewInclusions r) acc ps
+  where
+    addNewInclusions rhs a lhs =
+      F.foldl' addInclusion a $ simplifyInclusion (Inclusion lhs rhs)
+
+
+-- Cycle detection
+
+{-
+
+-- Track both a visited set and a "the nodes on the cycle" set
+checkChain :: Bool -> ConstraintEdge -> IFGraph -> Int -> Int -> Maybe IntSet
+checkChain False _ _ _ _ = Nothing
+checkChain True tgt g from to = do
+  chain <- snd $ checkChainWorker (mempty, Nothing) tgt g from to
+  return $ IS.insert from chain
+
+-- Only checkChainWorker adds things to the visited set
+checkChainWorker :: (IntSet, Maybe IntSet) -> ConstraintEdge -> IFGraph -> Int -> Int -> (IntSet, Maybe IntSet)
+checkChainWorker (visited, chain) tgt g from to
+  | from == to = (visited, Just (IS.singleton to))
+  | otherwise =
+    let visited' = IS.insert from visited
+    in G.foldPre (checkChainEdges tgt g to) (visited', chain) g from
+
+-- Once we have a branch of the DFS that succeeds, just keep that
+-- value.  This manages augmenting the set of nodes on the chain
+checkChainEdges :: ConstraintEdge
+                   -> IFGraph
+                   -> Int
+                   -> Int
+                   -> ConstraintEdge
+                   -> (IntSet, Maybe IntSet)
+                   -> (IntSet, Maybe IntSet)
+checkChainEdges _ _ _ _ _ acc@(_, Just _) = acc
+checkChainEdges tgt g to v lbl acc@(visited, Nothing)
+  | tgt /= lbl = acc
+  | IS.member v visited = acc
+  | otherwise =
+    -- If there was no hit on this branch, just return the accumulator
+    -- from the recursive call (which has an updated visited set)
+    case checkChainWorker acc tgt g v to of
+      acc'@(_, Nothing) -> acc'
+      (visited', Just chain) -> (visited', Just (IS.insert v chain))
+
+-- | Ask if we should bother to check for cycles this iteration
+checkCycles :: BuilderMonad v c Bool
+checkCycles = do
+  BuilderState _ _ cnt <- get
+  case cnt of
+    Nothing -> return True
+    Just c -> return $ c <= 1000
+
+-- FIXME: Maybe try to mark nodes as "exhausted" after they can't induce
+-- any new edges?
+--
+-- Also, perhaps use bitmasks instead of sets for something?
+
+-- | Try to detect cycles as in FFSA98.  Note that this is currently
+-- broken somehow.  It detects cycles just fine, but removing them
+-- seems to damage the constraint graph somehow making the solving
+-- phase much slower.
+tryCycleDetection :: (Ord c, Ord v) => Bool -> IFGraph
+                     -> Worklist -> ConstraintEdge
+                     -> Int -> Int -> BuilderMonad v c (IFGraph, Worklist)
+tryCycleDetection _ g2 affected Succ eid1 eid2 = simpleAddEdge g2 affected Succ eid1 eid2
+tryCycleDetection removeCycles g2 affected etype eid1 eid2 =
+  case checkChain removeCycles (otherLabel etype) g2 eid1 eid2 of
+    Just chain | not (IS.null chain) -> do
+      -- Make all of the nodes in the cycle refer to the min element
+      -- (the reference bit is taken care of in the node lookup and in
+      -- the result lookup).
+      --
+      -- For each of the nodes in @rest@, repoint their incoming and
+      -- outgoing edges.
+      BuilderState m v c <- get
+      -- Find all of the edges from any node pointing to a node in
+      -- @rest@.  Also find all edges from @rest@ out into the rest of
+      -- the graph.  Then resolve those back to inclusions using @v@
+      -- and call addInclusion over these new inclusions (after
+      -- blowing away the old ones)
+      let (representative, rest) = IS.deleteFindMin chain
+          thisExp = V.unsafeIndex v representative
+          newIncoming = IS.foldr' (srcsOf g2 v chain thisExp) [] rest
+          newInclusions = IS.foldr' (destsOf g2 v chain thisExp) newIncoming rest
+          g3 = IS.foldr' G.removeVertex g2 rest
+          m' = IS.foldr' (replaceWith v representative) m rest
+      put $! BuilderState m' v (fmap (+1) c)
+      foldM (addInclusion False) (g3, affected) newInclusions --  `debug`
+        -- ("Removing " ++ show (IS.size chain) ++ " cycle (" ++ show eid1 ++
+        --  " to " ++ show eid2 ++ "). " ++ show (CG.numNodes g3) ++
+        --  " nodes left in the graph.")
+      -- Nothing was affected because we didn't add any edges
+    _ -> simpleAddEdge g2 affected etype eid1 eid2
+  where
+    otherLabel Succ = Pred
+    otherLabel Pred = Succ
+
+srcsOf :: IFGraph -> Vector (SetExpression v c) -> IntSet
+          -> SetExpression v c -> Int -> [Inclusion v c]
+          -> [Inclusion v c]
+srcsOf g v chain newDst oldId acc =
+  G.foldPre (\srcId _ a ->
+              case IS.member srcId chain of
+                True -> a
+                False -> (V.unsafeIndex v srcId :<= newDst) : a) acc g oldId
+
+destsOf :: IFGraph -> Vector (SetExpression v c) -> IntSet
+          -> SetExpression v c -> Int -> [Inclusion v c]
+          -> [Inclusion v c]
+destsOf g v chain newSrc oldId acc =
+  G.foldSuc (\dstId _ a ->
+              case IS.member dstId chain of
+                True -> a
+                False -> (newSrc :<= V.unsafeIndex v dstId) : a) acc g oldId
+
+-- | Change the ID of the node with ID @i@ to @repr@
+replaceWith :: (Ord k) => Vector k -> a -> Int -> Map k a -> Map k a
+replaceWith v repr i m =
+  case M.lookup se m of
+    Nothing -> m
+    Just _ -> M.insert se repr m
+  where
+    se = V.unsafeIndex v i
+
+-}
diff --git a/src/Constraints/Set/Solver.hs b/src/Constraints/Set/Solver.hs
new file mode 100644
--- /dev/null
+++ b/src/Constraints/Set/Solver.hs
@@ -0,0 +1,75 @@
+-- | 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.
+module Constraints.Set.Solver (
+  -- * Constructors
+  emptySet,
+  universalSet,
+  setVariable,
+  term,
+  atom,
+  (<=!),
+  -- * Interface
+  solveSystem,
+  leastSolution,
+  -- * Types
+  ConstraintError(..),
+  Variance(..),
+  Inclusion,
+  SetExpression(..),
+  SolvedSystem
+  ) where
+
+import Constraints.Set.Implementation
diff --git a/tests/ConstraintTests.hs b/tests/ConstraintTests.hs
new file mode 100644
--- /dev/null
+++ b/tests/ConstraintTests.hs
@@ -0,0 +1,259 @@
+module Main ( main ) where
+
+import Control.Exception
+import Data.List ( permutations, sort )
+import Test.Framework ( defaultMain, testGroup, Test )
+import Test.Framework.Providers.HUnit
+import Test.HUnit hiding ( Test )
+
+import Constraints.Set.Solver
+
+tests :: [Test]
+tests = [
+  testGroup "Simple" [
+     testCase "tc1" tc1,
+     testCase "tc2" tc2,
+     testCase "tc3" tc3,
+     testCase "tc4" tc4,
+     testCase "tc5" tc5,
+     testCase "tc6" tc6,
+     testCase "tc7" tc7,
+     testCase "tc8" tc8,
+     testCase "tc9" tc9,
+     testCase "tc10" tc10,
+     testCase "tc11" tc11
+     ],
+  testGroup "PointsTo" [
+    testCase "pt1" pt1,
+    testCase "pt2" pt2
+    ]
+  ]
+
+tc1 :: Assertion
+tc1 = solveFor "tc1" "a" [5,6] is
+  where
+    is = [ atom 5 <=! setVariable "a", atom 6 <=! setVariable "a" ]
+
+tc2 :: Assertion
+tc2 = solveFor "tc2" "a" [5] is
+  where
+    is = [ atom 5 <=! setVariable "a", atom 6 <=! setVariable "b" ]
+
+tc3 :: Assertion
+tc3 = solveFor "tc3" "a" [5,6] is
+  where
+    is = [ atom 5 <=! setVariable "b"
+         , atom 6 <=! setVariable "b"
+         , setVariable "b" <=! setVariable "a"
+         ]
+
+tc4 :: Assertion
+tc4 = solveFor "tc4" "a" [0..20] is
+  where
+    is = map ((<=! setVariable "a") . atom) [0..20]
+
+-- | From the FFSA98 paper
+tc5 :: Assertion
+tc5 = mapM_ (solveFor "tc5" "R1" [0..40]) $ take 1000 $ permutations is
+  where
+    is = concat [
+      [ setVariable "Z" <=! setVariable "R1"
+      , setVariable "Z" <=! setVariable "R2"
+      , setVariable "Y1" <=! setVariable "Z"
+      , setVariable "Y2" <=! setVariable "Z"
+      , setVariable "X" <=! setVariable "Y1"
+      , setVariable "X" <=! setVariable "Y2"
+      , setVariable "L1" <=! setVariable "X"
+      , setVariable "L2" <=! setVariable "X"
+      ],
+      map ((<=! setVariable "L1") . atom) [0..20],
+      map ((<=! setVariable "L2") . atom) [20..40]
+      ]
+
+-- | Test a simple cycle
+tc6 :: Assertion
+tc6 = mapM_ (solveFor "tc6" "a" [5,6,7,8]) $ take 1000 $ permutations is
+  where
+    is = [ atom 5 <=! setVariable "b"
+         , atom 6 <=! setVariable "b"
+         , atom 7 <=! setVariable "a"
+         , atom 8 <=! setVariable "a"
+         , setVariable "b" <=! setVariable "a"
+         , setVariable "a" <=! setVariable "b"
+         ]
+
+-- | Test a longer cycle
+tc7 :: Assertion
+tc7 = mapM_ (solveFor "tc7" "f" [5,6,7,8]) $ take 1000 $ permutations is
+  where
+    is = [ atom 5 <=! setVariable "b"
+         , atom 6 <=! setVariable "b"
+         , atom 7 <=! setVariable "a"
+         , atom 8 <=! setVariable "a"
+         , setVariable "b" <=! setVariable "a"
+         , setVariable "c" <=! setVariable "b"
+         , setVariable "d" <=! setVariable "c"
+         , setVariable "e" <=! setVariable "d"
+         , setVariable "f" <=! setVariable "e"
+         , setVariable "g" <=! setVariable "f"
+         , setVariable "a" <=! setVariable "g"
+         ]
+
+
+tc8 :: Assertion
+tc8 = mapM_ (solveFor "tc8" "zz" []) $ take 1000 $ permutations is
+  where
+    is = [ atom 5 <=! setVariable "b"
+         , atom 6 <=! setVariable "b"
+         , atom 7 <=! setVariable "a"
+         , atom 8 <=! setVariable "a"
+         , setVariable "b" <=! setVariable "a"
+         , setVariable "c" <=! setVariable "b"
+         , setVariable "d" <=! setVariable "c"
+         , setVariable "e" <=! setVariable "d"
+         , setVariable "f" <=! setVariable "e"
+         , setVariable "g" <=! setVariable "f"
+         , setVariable "a" <=! setVariable "g"
+         , setVariable "z" <=! setVariable "f"
+         , setVariable "zz" <=! setVariable "z"
+         ]
+
+tc9 :: Assertion
+tc9 =
+  mapM_ (solveFor "tc9" "zz" [11]) $ take 1000 $ permutations is
+  where
+    is = [ atom 5 <=! setVariable "b"
+         , atom 6 <=! setVariable "b"
+         , atom 7 <=! setVariable "a"
+         , atom 8 <=! setVariable "a"
+         , setVariable "b" <=! setVariable "a"
+         , setVariable "c" <=! setVariable "b"
+         , setVariable "d" <=! setVariable "c"
+         , setVariable "e" <=! setVariable "d"
+         , setVariable "f" <=! setVariable "e"
+         , setVariable "g" <=! setVariable "f"
+         , setVariable "a" <=! setVariable "g"
+         , setVariable "z" <=! setVariable "f"
+         , setVariable "zz" <=! setVariable "z"
+         , atom 11 <=! setVariable "zz"
+         ]
+
+tc10 :: Assertion
+tc10 =
+  mapM_ (solveFor "tc10" "c" [5,6,7,8,11]) $ take 1000 $ permutations is
+  where
+    is = [ atom 5 <=! setVariable "b"
+         , atom 6 <=! setVariable "b"
+         , atom 7 <=! setVariable "a"
+         , atom 8 <=! setVariable "a"
+         , setVariable "b" <=! setVariable "a"
+         , setVariable "c" <=! setVariable "b"
+         , setVariable "d" <=! setVariable "c"
+         , setVariable "e" <=! setVariable "d"
+         , setVariable "f" <=! setVariable "e"
+         , setVariable "g" <=! setVariable "f"
+         , setVariable "a" <=! setVariable "g"
+         , setVariable "z" <=! setVariable "f"
+         , setVariable "zz" <=! setVariable "z"
+         , atom 11 <=! setVariable "zz"
+         ]
+
+-- | There are no solutions to this type of constraint (A ⊆ c) when c is
+-- a nullary constructor (a constant term).  It can have solutions
+-- when c has arguments.
+tc11 :: Assertion
+tc11 = solveFor "tc11" "a" [] is
+  where
+    is = [ setVariable "a" <=! atom 5 ]
+
+solveFor :: String -> String -> [Int] -> [Inclusion String Int] -> Assertion
+solveFor name var expected is =
+  assertEqual name (sort (map toSetExp expected)) (sort sol)
+  where
+    Just solved = solveSystem is
+    Just sol = leastSolution solved var
+
+toSetExp :: (Ord v) => Int -> SetExpression v Int
+toSetExp i = term i [] []
+
+-- | Points-to example from the paper, a = &b;
+pt1 :: Assertion
+pt1 = assertEqual "pt1" [loc "b"] sol
+  where
+    sol = either throwErr id $ do
+      s <- solveSystem is
+      leastSolution s "Xa"
+    ref = term "ref" [Covariant, Covariant, Contravariant]
+    loc name = ref [atom name, setVariable ("X"++name), setVariable ("X"++name)]
+    is = [ loc "a" <=! ref [ universalSet, universalSet, setVariable "T1" ]
+         , ref [ emptySet, loc "b", emptySet ] <=! ref [ universalSet, setVariable "T2", emptySet ]
+         , setVariable "T2" <=! setVariable "T1"
+         ]
+
+
+-- | A simple example (with LLVM bitcode)
+-- > int * p1, *p2;
+-- > int ** pp;
+-- > int x,y,z;
+-- >
+-- > p1 = &x;
+-- > p2 = &y;
+-- > pp = &p2;
+-- > *pp = p1;
+-- > *pp = &z;
+--
+-- > store i32* @x, i32** @p1, align 4
+-- > store i32* @y, i32** @p2, align 4
+-- > store i32** @p2, i32*** @pp, align 4
+-- > %1 = load i32** @p1, align 4
+-- > %2 = load i32*** @pp, align 4
+-- > store i32* %1, i32** %2, align 4
+-- > %3 = load i32*** @pp, align 4
+-- > store i32* @z, i32** %3, align 4
+pt2 :: Assertion
+pt2 = assertEqual "pt2" (sort [loc "x", loc "z"]) (sort sol)
+  where
+    sol = either throwErr id $ do
+      s <- solveSystem is
+      leastSolution s "Xp1"
+    ref = term "ref" [Covariant, Covariant, Contravariant]
+    loc name = ref [atom name, setVariable ("X"++name), setVariable ("X"++name)]
+
+    xloc = loc "x"
+    yloc = loc "y"
+    zloc = loc "z"
+    p1loc = loc "p1"
+    p2loc = loc "p2"
+    pploc = loc "pp"
+    -- First, p1 = &x
+    is = [ loc "p1" <=! ref [ universalSet, universalSet, setVariable "T1" ]
+         , ref [ emptySet, loc "x", emptySet ] <=! ref [ universalSet, setVariable "T2", emptySet ]
+         , setVariable "T2" <=! setVariable "T1"
+           -- now p2 = &y
+         , loc "p2" <=! ref [ universalSet, universalSet, setVariable "T3" ]
+         , ref [ emptySet, loc "y", emptySet ] <=! ref [universalSet, setVariable "T4", emptySet ]
+         , setVariable "T4" <=! setVariable "T3"
+           -- now pp = &p2;
+         , loc "pp" <=! ref [ universalSet, universalSet, setVariable "T5" ]
+         , ref [ emptySet, loc "p2", emptySet ] <=! ref [universalSet, setVariable "T6", emptySet ]
+         , setVariable "T6" <=! setVariable "T5"
+           -- now pp = &p1;
+         , loc "pp" <=! ref [ universalSet, universalSet, setVariable "T7" ]
+         , ref [ emptySet, loc "p1", emptySet ] <=! ref [universalSet, setVariable "T8", emptySet ]
+         , setVariable "T8" <=! setVariable "T7"
+           -- *pp (saved as T9)
+         , loc "pp" <=! ref [ universalSet, setVariable "T9", emptySet ]
+           -- *pp = &z;
+         , setVariable "T9" <=! ref [ universalSet, universalSet, setVariable "TT" ]
+         , ref [ emptySet, loc "z", emptySet ] <=! ref [universalSet, setVariable "T10", emptySet ]
+         , setVariable "T10" <=! setVariable "TT"
+         ]
+
+-- What if we take the above and add *pp = &zz; (make sure to just
+-- re-use T9).  Another important case, what about *pq = *pp;
+
+throwErr :: ConstraintError String String -> [SetExpression String String]
+throwErr = throw
+
+main :: IO ()
+main = defaultMain tests