packages feed

ifscs (empty) → 0.2.0.0

raw patch · 6 files changed

+854/−0 lines, 6 filesdep +HUnitdep +basedep +containerssetup-changed

Dependencies added: HUnit, base, containers, failure, ifscs, test-framework, test-framework-hunit

Files

+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ifscs.cabal view
@@ -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
+ src/Constraints/Set/Implementation.hs view
@@ -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++-}
+ src/Constraints/Set/Solver.hs view
@@ -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
+ tests/ConstraintTests.hs view
@@ -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