obdd 0.3.3 → 0.4.0

raw patch · 7 files changed

+381/−16 lines, 7 filesdep +processdep ~basedep ~containersPVP ok

version bump matches the API change (PVP)

Dependencies added: process

Dependency ranges changed: base, containers

API changes (from Hackage documentation)

Files

• examples/Queens2.hs +69/−0
• examples/Sort.hs +234/−0
• obdd.cabal +14/−2
• src/OBDD.hs +6/−5
• src/OBDD/Data.hs +13/−4
• src/OBDD/Make.hs +9/−1
• src/OBDD/Operation.hs +36/−4

@@ -0,0 +1,69 @@+{-+the N Queens problem (alternative implementation).+The propositional variables+correspond to the positions on the board.+It shows how to construct an OBDD+and how to check some of its properties.+It also shows that the implementation is not terribly efficient.+It computes the number of solutions for board size 8+(the answer is: 92) in approx. 1.6 seconds on my machine.++BUILD:  ghc -O2 Queens+RUN  :  ./Queens 8+-}++import Prelude hiding ((&&),(||),not,and,or)+import OBDD ++import Control.Monad ( guard )+import System.Environment ( getArgs )+import qualified Data.Set +import qualified Data.Map.Strict as M++type Position = (Int,Int)++positions :: Int -> [ Position ]+positions n = do +    a <- [ 1 .. n ]+    b <- [ 1 .. n ]+    return (a,b)++board :: Int -> OBDD Position+board n = and +    [ handle exactlyone (\(x,y) -> x) n+    , handle atmostone  (\(x,y) -> y) n+    , handle atmostone  (\(x,y) -> x+y) n+    , handle atmostone  (\(x,y) -> x-y) n+    ]++atmostone xs =+  let go (n,o) [] = n || o+      go (n,o) (x:xs) = go (bool n false x, bool o n x) xs+  in  go (true,false) xs++exactlyone xs =+  let go (n,o) [] = o+      go (n,o) (x:xs) = go (bool n false x, bool o n x) xs+  in  go (true,false) xs++handle check f n = OBDD.and $ do+    (k,v) <- M.toList $ M.fromListWith (++)+          $ map (\p -> (f p, [variable p])) $ positions n+    return $ check v++main = do+    args <- getArgs+    case map read args :: [Int] of+        [] -> mainf 8+        [arg] -> mainf arg++mainf n = do+    let d :: OBDD Position+        d = board n+    putStrLn $ unwords [ "board size", show n ]+    putStrLn $ unwords [ "BDD size", show $ OBDD.size d ]+    putStrLn $ unwords [ "number of models"+                       , show $ OBDD.number_of_models +                         ( Data.Set.fromList $ positions n )+                         d+                       ]

@@ -0,0 +1,234 @@+{-# language LambdaCase #-}++import Prelude hiding ((&&),(||),not,and,or,Num)+import qualified Prelude+import qualified Data.Bool +import OBDD hiding (size)+import qualified OBDD as O++import Control.Monad ( guard, forM_, when, void, mzero, msum )+import System.Environment ( getArgs )+import System.IO (hFlush, stdout)+import qualified Data.Set as S+import qualified Data.Map.Strict as M+import Data.List (sort, sortOn, tails, transpose)+import qualified Data.Tree as T+import Data.Maybe (isJust)++import Debug.Trace++-- | we will talk about permutation matrices,+-- so we need to index their elements.+type Bit = OBDD (Int,Int)++ispermutation :: [[Bit]] -> Bit+ispermutation xss =+     ( and $ map exactlyone xss )+  && ( and $ map exactlyone $ transpose xss )++exactlyone :: [Bit] -> Bit+exactlyone xs =+  let go (n,o) [] = o+      go (n,o) (x:xs) = go (bool n false x, bool o n x) xs+  in  go (true,false) xs++-- | (weakly) increasing sequence of bits+type Num = [Bit] ++-- | produce a number from a sequence that has exactly one bit set.+number :: [Bit] -> [Bit]+number (x:xs) = scanl (||) x xs++lt :: Num -> Num -> Bit+lt xs ys = or $ zipWith (\x y -> not x && y) xs ys++leq :: Num -> Num -> Bit+leq xs ys = and $ zipWith implies xs ys++type Comp = (Int,Int)++comparators :: Int -> [Comp]+comparators w =+  [0 .. w-2] >>= \ x -> [x+1..w-1] >>= \ y -> [(x,y)]++compat :: [Num] -> Comp -> Bit+compat ns (lo,hi) = leq (ns !! lo) (ns !! hi)++input w = do+  i <- [1..w]+  return $ map (\j -> variable (i,j))[1..w]++vars w = S.fromList $ (,) <$> [1..w] <*> [1..w]++-- * poset enumeration++data State =+     State { comps:: ! [Comp]+           , poset :: ! Poset+           , args :: ! [Num]+           , form :: ! Bit+           , size :: ! Integer+           }++start w =+  let i = input w+      f = ispermutation i+  in State { comps = []+           , poset = mkposet []+           , args = map number i+           , form = f+           , size = number_of_models (vars w) f+           }++next :: Int -> State -> Comp -> State+next w s c =+  let cs' = c : comps s+      f = compat (args s) c && form s+  in  s { comps = cs'+        , poset = -- mkposet cs'+	    transitive_closure $ S.insert c $ poset s+        , form = f+        , size = number_of_models (vars w) f+        }++run w d = do+  putStrLn $ unwords [ "sort", show w, "items", "with", show d, "comparisons" ]+  (r, cache) <- work w d (start w) M.empty+  putStrLn ""+  putStrLn $ unwords [ "sort", show w, "items", "with", show d, "comparisons", "is"+     , Data.Bool.bool "IMPOSSIBLE" "POSSIBLE" r ]+  putStrLn $ unwords [ "cache", "with", show (M.size cache), "entries" ]+  when False $ forM_ (M.toList cache) $ \(k,v) -> do+    putStrLn $ unwords [ show k, "=>", show v ]+    -- forM_ (M.toList m) print+  return r++work w d s known = do+  -- print (d,comps s,size s)+  if size s == 1+    then return (True,known)+    else if size s > 2^d+         then return (False,known)+         else do+	   let verbose = False+           case M.lookup (canonical $ poset s) known of+             Just (r,prev) -> do+               if verbose+	         then putStrLn $ unwords [ show d, show $ size s, show (comps s)+                                  , show r, "iso", show prev ]+		 else putStr "!"+               return (r,known)+             Nothing -> do+               let go [] known = return (False, known)+                   go (c@(x,y):cs) known = do+		     let [s1,s2] = reverse+		                 $ sortOn size+		                 $ map (next w s) [ (x,y), (y,x) ]+                     (a1,k1) <- work w (d-1) s1 known+                     if a1+                       then do+                         (a2,k2) <- work w (d-1) s2 k1+                         if a2+                           then return (True, k2)+                           else go cs k2+                       else do+                         go cs k1+               let candidates =+                     filter (\ (x,y) -> Prelude.not $ S.member (x,y) $ poset s)+                     $ filter (\ (x,y) -> Prelude.not $ S.member (y,x) $ poset s)+                      $ comparators w+               (r,known) <- go candidates known+               if verbose+	         then putStrLn $ unwords [ show d, show $ size s, show (comps s)+                                  , show r ]+                 else putStr "." +  	       hFlush stdout	 +               return+                 (r, M.insert (canonical $ poset s) (r, comps s) known)++-- * main++main = getArgs >>= \ case+  [ ] -> void $ run 4 5+  [ w ] -> let b = ceiling+                 $ logBase 2 $ fromIntegral+                 $ factorial $ read w+           in -- search (read w) b+	       void $ run (read w) b+  [ w , d ] -> void $ run (read w) (read d)+++search w d = run w d >>= \ case+  True -> return ()+  False -> search w (d+1)+  +factorial n = product [1 .. n]++-- * posets and their isomorphisms++type Poset = S.Set Comp++mkposet comps = transitive_closure $ S.fromList comps++dot :: Poset -> Poset -> Poset+dot p q = S.fromList $ do+  (x,y1) <- S.toList p+  (y2,z) <- S.toList q+  guard $ y1 == y2+  return (x,z)++transitive_closure :: Poset -> Poset+transitive_closure p =+  let q = S.union p $ dot p p+  in  if p == q then p else transitive_closure q+      +inputs  p x = map fst $ filter ((== x) . snd) $ S.toList p+outputs p x = map snd $ filter ((== x) . fst) $ S.toList p++elements p = S.union ( S.map fst p ) (S.map snd p )++-- | the Int is the length, and it is used to speed up+-- the derived Eq and Ord instance.+data List a = List !Int ![a] deriving (Eq, Ord, Show)++nil :: List a+nil = List 0 []++cons :: a -> List a -> List a+cons x (List n xs) = List (n+1) (x:xs)++list :: [a] -> List a+list xs = List (length xs) xs++instance Functor List where+  fmap f (List n xs) = List n (map f xs)++data Type = Dot | Type (List Type) (List Type) deriving (Eq, Ord, Show)++types :: Poset -> M.Map Int Type+types p = M.fromList $ zip (S.toList $ elements p) $ repeat Dot++refine :: Poset ->   M.Map Int Type -> M.Map Int Type+refine p t = M.fromList $ do+  x <- S.toList $ elements p+  return (x, Type ( list $ sort $ map (t M.!) $ inputs  p x )+                  ( list $ sort $ map (t M.!) $ outputs p x ) )++classes :: M.Map Int Type -> M.Map Type (S.Set Int)+classes m = M.fromListWith S.union $ do+  (k,v) <- M.toList m+  return (v, S.singleton k)++-- | compare with keys+essence t = M.toAscList $ M.map S.size $ classes t++canonical po =+  let go t p =+        let t' = refine po t+            c' = classes t+            p' = sort $ M.elems c'+        in  if p == p' then M.map S.size c' else go t' p'+  in  go (types po) []+++               

@@ -1,5 +1,5 @@ Name:                obdd-Version:             0.3.3+Version:             0.4.0 Cabal-Version:       >= 1.8 Build-type: Simple Synopsis:            Ordered Reduced Binary Decision Diagrams@@ -17,7 +17,7 @@     Location: git://github.com/jwaldmann/haskell-obdd.git  Library-    Build-Depends:       base==4.*, random, mtl, containers>=0.5, array+    Build-Depends:       base==4.*, random, mtl, containers>=0.5, array, process     Hs-Source-Dirs:	     src     Exposed-Modules:     OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property     Other-Modules:	     OBDD.IntIntMap, OBDD.VarIntIntMap@@ -35,4 +35,16 @@     Main-Is: Queens.hs     Build-Depends: base, containers, obdd +test-suite obdd-queens2+    Hs-Source-Dirs : examples+    Type: exitcode-stdio-1.0+    Main-Is: Queens2.hs+    Build-Depends: base, containers, obdd+    +test-suite obdd-sort+    Hs-Source-Dirs : examples+    Type: exitcode-stdio-1.0+    Main-Is: Sort.hs+    Build-Depends: base, containers, obdd+    Ghc-Options: -rtsopts     

@@ -1,16 +1,17 @@--- | reduced ordered binary decision diagrams+-- | Reduced ordered binary decision diagrams,+-- pure Haskell implementation. -- (c) Johannes Waldmann, 2008 ----- this module is intended to be imported qualified+-- This module is intended to be imported qualified -- because it overloads some Prelude names. ----- for a similar, but much more elaborate project, see+-- For a similar, but much more elaborate project, see -- <http://www.informatik.uni-kiel.de/~mh/lehre/diplomarbeiten/christiansen.pdf> -- but I'm not sure where that source code would be available.  module OBDD  -( OBDD +( OBDD, display , module OBDD.Property , module OBDD.Operation , module OBDD.Make@@ -18,7 +19,7 @@  where -import OBDD.Data ( OBDD )+import OBDD.Data ( OBDD, display ) import OBDD.Property import OBDD.Operation import OBDD.Make

@@ -15,7 +15,7 @@ , number_of_models , some_model, all_models , fold, foldM-, toDot+, toDot, display -- * for internal use , Node (..) , make@@ -49,9 +49,10 @@    (State, runState, evalState, get, put, gets, modify) import qualified System.Random import Control.Monad.Fix-import Control.Monad ( forM, guard )+import Control.Monad ( forM, guard, void ) import qualified Control.Monad ( foldM )-+import System.Process+import Data.List (isPrefixOf, isSuffixOf)  import Prelude hiding ( null ) import qualified Prelude@@ -277,6 +278,11 @@       register n     _ -> register n +-- | Calls the @dot@ executable (must be in @$PATH@) to draw a diagram+-- in an X11 window. Will block until this window is closed.+-- Window can be closed gracefully by typing  'q'  when it has focus.+display :: Show v => OBDD v -> IO ()+display d = void $ readProcess "dot" [ "-Tx11" ] $ toDot d  -- | toDot outputs a string in format suitable for input to the "dot" program -- from the graphviz suite.@@ -296,7 +302,10 @@                           _ -> idmap IM.! i         in id &&& getNode -    mkLabel lbl = "[label=\"" ++ lbl ++ "\"];"+    unquote s = if isPrefixOf "\"" s && isSuffixOf "\"" s+                then init $ tail s+                else s+    mkLabel lbl = "[label=\"" ++ unquote lbl ++ "\"];"      helper (thisId, Leaf b) = return $         -- switch to rectangle nodes for the leaf, before going back to ovals.

@@ -2,7 +2,7 @@  module OBDD.Make  -( constant, unit )+( constant, unit, variable, false, true )  where @@ -15,6 +15,12 @@ constant b = make $ do     register $ Leaf b +false :: Ord v => OBDD v+false = constant False++true :: Ord v => OBDD v+true  = constant True+ -- | Variable with given parity unit :: Ord v => v -> Bool -> OBDD v unit v p = make $ do@@ -22,3 +28,5 @@     r <- register $ Leaf $     p     register $ Branch v l r +variable :: Ord v => v -> OBDD v+variable v = unit v True

@@ -1,8 +1,10 @@ {-# language ScopedTypeVariables #-}+{-# language PatternGuards #-}  module OBDD.Operation   ( (&&), (||), not, and, or+, bool, implies, equiv, xor , unary, binary , instantiate , exists, exists_many@@ -23,17 +25,31 @@ -- import Data.List ( foldl' ) -- don't use, see below -import Prelude hiding ( (&&), (||), and, or, not )+import Prelude hiding ( (&&), (||), and, or, not, bool ) import qualified Prelude +infixr 3 &&+ ( && ) :: Ord v => OBDD v -> OBDD v -> OBDD v-( && ) = binary ( Prelude.&& )+( && ) = symmetric_binary ( Prelude.&& ) +infixr 2 ||+ ( || ) :: Ord v => OBDD v -> OBDD v -> OBDD v-( || ) = binary ( Prelude.|| )+( || ) = symmetric_binary ( Prelude.|| ) +bool :: Ord v => OBDD v -> OBDD v -> OBDD v -> OBDD v+bool f t p = (f && not p) || (t && p) +equiv :: Ord v => OBDD v -> OBDD v -> OBDD v+equiv = symmetric_binary (==) +xor :: Ord v => OBDD v -> OBDD v -> OBDD v+xor   = symmetric_binary (/=)++implies :: Ord v => OBDD v -> OBDD v -> OBDD v+implies = binary ( <= )+ and :: Ord v => [ OBDD v ] -> OBDD v and = fold_by_size (constant True) (&&) -- and = foldr ( && ) ( constant True ) @@ -75,11 +91,27 @@     handle x  +data Symmetricity = Asymmetric | Symmetric deriving Show+ binary :: Ord v       => ( Bool -> Bool -> Bool )       -> OBDD v -> OBDD v -> OBDD v-binary op x y = make $ do+binary = binary_ Asymmetric+      +symmetric_binary :: Ord v+      => ( Bool -> Bool -> Bool )+      -> OBDD v -> OBDD v -> OBDD v+symmetric_binary = binary_ Symmetric+++binary_ :: Ord v+      => Symmetricity+      -> ( Bool -> Bool -> Bool )+      -> OBDD v -> OBDD v -> OBDD v++binary_ sym op x y = make $ do     let -- register = checked_register -- for testing+        -- handle x y | Symmetric <- sym, top x > top y = handle y x         handle x y = cached (top x, top y) $ case ( access x , access y ) of                     ( Leaf p , Leaf q ) -> register $ Leaf $ op p q                     ( ax, ay ) -> case comp ax ay of