obdd 0.8.1 → 0.8.2

raw patch · 6 files changed

+196/−70 lines, 6 filesdep ~basedep ~containersPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base, containers

API changes (from Hackage documentation)

Files

• examples/Domino.hs +88/−0
• examples/Weight.hs +2/−5
• obdd.cabal +21/−11
• src/OBDD/Data.hs +24/−35
• src/OBDD/IntIntMap.hs +4/−1
• src/OBDD/Operation.hs +57/−18

@@ -0,0 +1,88 @@+{-+In how many ways can a n x m board be entirely covered by 2 x 1 domino+pieces?++Usage: ./Domino 4 3+       time stack runghc examples/Domino.hs 4 9+       VERBOSE=1 stack runghc examples/Domino.hs 2 3+   or: ghci> prettySolve 4 3+-}+module Main where++import Prelude hiding (bool,not,and,or,any,all,(&&),(||))+import Control.Monad (guard, when)+import Data.Maybe (isJust)+import System.Environment (getArgs, lookupEnv)+import qualified Data.Map+import qualified Data.Set+import Data.List (tails)++import Prelude hiding ((&&),(||),not,and,or,all,any)+import OBDD++dominoes w h = rows ++ cols+    where rows = positions [1..h-1] [1..w] $ \x y -> ((x, y), (x+1, y))+          cols = positions [1..h] [1..w-1] $ \x y -> ((x, y), (x, y+1))+          positions xs ys f = f <$> xs <*> ys++positions w h = (,) <$> [1..h] <*> [1..w]++dominoFormula w h =+  all ( \ f -> exactly_one (map variable $ filter (isCoveredBy f) (dominoes w h) )+      ) (positions w h)++f `isCoveredBy` p = f == fst p || f == snd p++exactly_one xs = or xs && atmost_one xs++atmost_one :: Boolean b => [b] -> b+atmost_one = atmost_one_lin++atmost_one_lin xs =+  let go [] = (true,false)+      go [x] = (not x, x)+      go xs = let (ys,zs) = splitAt (div (length xs) 2) xs+                  (y0,y1) = go ys+		  (z0,z1) = go zs+              in  (y0 && z0, y1 && z0 || y0 && z1)+      (x0,x1) = go xs+  in  x0 || x1++atmost_one_quad xs = not $ or $ do+  p <- xs ; q <- xs ; guard $ p < q+  return $ and [ OBDD.unit p True, OBDD.unit q True ]+++prettySolution w h ds = putStr $ concat $ do+    x <- [1..h]+    y <- [1..w]+    let letter = case find (\(domino, _) -> fst domino == (x, y) || snd domino == (x, y)) withNames of+                     Nothing -> "."+                     Just (_, letter) -> letter:[]+    return $ if y == w then letter ++ "\n" else letter+    where withNames = if length names < length ds+                      then error "not enough names"+                      else zip ds names+          names = ['0'..'9'] ++ ['a'..'z'] ++ ['A'..'Z']+          find f xs = case filter f xs of+                          []  -> Nothing+                          x:_ -> Just x++prettySolve w h =+    mapM_ (\ds -> prettySolution w h ds >> putStrLn "")+    . map (map fst . filter snd)+    . map (Data.Map.toList) $+    models (Data.Set.fromList $ dominoes w h) $ dominoFormula w h++main = do+    args <- getArgs+    let [width, height] = case map read args :: [Int] of+              [] -> [4, 3]+              [width, height] -> [width, height]+    let formula = dominoFormula width height+    verbose <- lookupEnv "VERBOSE" >>= return . isJust+    when verbose $ mapM_ (\ds -> prettySolution width height ds >> putStrLn "")+                   . map (map fst . filter snd)+                   . map (Data.Map.toList) $+                   models (Data.Set.fromList $ dominoes width height) formula+    print $ number_of_models (Data.Set.fromList $ dominoes width height) formula

@@ -1,10 +1,7 @@ {- -NOTE: the following comment is lying, see https://github.com/jwaldmann/haskell-obdd/issues/5--The minimal number of knights needed to occupy or attack-every square on an n×n chessboard-(i.e., domination numbers for the n×n knight graphs)+The maximal number of non-attacking knights on an n×n chessboard+(i.e., independence numbers for the n×n knight graphs)  http://mathworld.wolfram.com/KnightsProblem.html 

@@ -1,5 +1,5 @@ Name:                obdd-Version:             0.8.1+Version:             0.8.2 Cabal-Version:       >= 1.8 Build-type: Simple Synopsis:            Ordered Reduced Binary Decision Diagrams@@ -13,25 +13,29 @@   An important (for me, in teaching) feature is   that I can immediately draw the BDD to an X11 window (via graphviz).   For example, to show the effect of different variable orderings,-  try this in ghci:+  try this in ghci (type 'q' to close the drawing windows).   .-  > import qualified Prelude as P+  > import Prelude hiding (not,(&&),(||),and,or,any,all)   > import OBDD   > let f [] = false; f (x:y:zs) = x && y || f zs-  > display P.$ f P.$ P.map variable [1,2,3,4,5,6]-  > display P.$ f P.$ P.map variable [1,4,2,5,3,6]+  > display $ f $ map variable [1,2,3,4,5,6]+  > display $ f $ map variable [1,4,2,5,3,6]   .-  If you want better performance,-  use <http://vlsi.colorado.edu/%7Efabio/CUDD/ CUDD>+  'OBDD' implements 'Ersatz.Boolean' which re-defines+  Boolean operations from the Prelude. The recommended way of using this+  is shown in the previous example.+  .+  If you want better performance, use a library with a persistent BDD base,+  e.g., <http://vlsi.colorado.edu/%7Efabio/CUDD/ CUDD>   <https://hackage.haskell.org/package/cudd Haskell bindings>,   see <https://gitlab.imn.htwk-leipzig.de/waldmann/min-comp-sort this example>. -category:	     Logic+category:            Logic License:             GPL License-file:        LICENSE Author:              Johannes Waldmann Maintainer:          Johannes Waldmann-Homepage:	     https://github.com/jwaldmann/haskell-obdd+Homepage:            https://github.com/jwaldmann/haskell-obdd  Source-Repository head     Type: git@@ -39,15 +43,21 @@  Library     Build-Depends:       base==4.*, random, mtl, containers>=0.5, array, process-extras, ersatz, text-    Hs-Source-Dirs:	     src+    Hs-Source-Dirs:          src     Exposed-Modules:     OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property, OBDD.Display, OBDD.Linopt, OBDD.Cube-    Other-Modules:	     OBDD.IntIntMap, OBDD.VarIntIntMap+    Other-Modules:           OBDD.IntIntMap, OBDD.VarIntIntMap     ghc-options: -funbox-strict-fields  test-suite obdd-placement     Hs-Source-Dirs : examples     Type: exitcode-stdio-1.0     Main-Is: Placement.hs+    Build-Depends: base, containers, obdd++test-suite obdd-domino+    Hs-Source-Dirs: examples+    Type: exitcode-stdio-1.0+    Main-Is: Domino.hs     Build-Depends: base, containers, obdd  test-suite obdd-cubism

@@ -22,9 +22,10 @@ , Node (..) , make , register, checked_register-, cached, top+, top , access-+, not_+, assocs )  where@@ -71,14 +72,14 @@                          -- , icore :: !(Map ( Node v Index ) Index)             , icore :: !(VarIntIntMap v Index)+            , ifalse :: ! Index+            , itrue :: ! Index             , next :: !Index             , top :: !Index-            -            , cache ::  !(IntIntMap Index) -               -- ^ inputs and output for binary op-               -- (unary will be simulated by binary)             } +assocs :: OBDD v -> [(Index, Node v Index)]+assocs o = IM.toAscList $ core o  -- | Apply function in each node, bottom-up. -- return the value in the root node.@@ -104,15 +105,13 @@      -> ( v -> a -> a -> m a )      -> OBDD v -> m a foldM leaf branch o = do-    f <- leaf False ; t <- leaf True-    let m0 = M.fromList -           [(icore_false,f), (icore_true,t)]     m <- Control.Monad.foldM ( \ m (i,n) -> do             val <- case n of+                Leaf b -> leaf b                 Branch v l r ->                          branch v (m M.! l) (m M.! r)              return $ M.insert i val m-          ) m0 $ IM.toAscList $ core o+          ) M.empty $ IM.toAscList $ core o     return $ m M.! top o  -- | Apply function in each node, bottom-up.@@ -158,9 +157,6 @@           ) o     interpolate a Nothing res   -icore_false = 0 :: Index  -icore_true = 1 :: Index  -               size = unIndex . next  -- | Number of satisfying assignments with  given set of variables.@@ -173,21 +169,29 @@  empty :: OBDD v empty = OBDD -      { core = IM.empty+      { core = IM.fromList [(0,Leaf False),(1,Leaf True)]       , icore = VIIM.empty+      , ifalse = 0+      , itrue = 1       , next = 2-      , top = 0-      , cache = IIM.empty+      , top = -1       }  data Node v i = Leaf !Bool             | Branch !v !i !i     deriving ( Eq, Ord ) +not_ o = o { ifalse = itrue o+           , itrue = ifalse o+           , core = IM.insert (itrue o) (Leaf False)+                  $ IM.insert (ifalse o) (Leaf True)+                  $ core o+           }+ access :: OBDD v -> Node v ( OBDD v ) access s = case top s of-    0 -> Leaf False-    1 -> Leaf True+    i | i == ifalse s -> Leaf False+    i | i == itrue s -> Leaf True     t -> case IM.lookup ( top s ) ( core s ) of         Nothing -> error "OBDD.Data.access"         Just n  -> case n of@@ -261,27 +265,12 @@     put $! s { next = succ i }     return i -cached :: Ord v-        => (Index, Index) -        -> ( State ( OBDD v ) Index )-        -> State ( OBDD v ) Index-cached (l,r) action = do-    s <- get-    case IIM.lookup (l, r) $ cache s of-        Just i -> return i-        Nothing -> do-            i <- action-            s <- get-            put $! s { cache = IIM.insert (l, r) i -                              $ cache s }-            return i- register :: Ord v          => Node v Index        -> State ( OBDD v ) Index register n = case n of-    Leaf False -> return 0-    Leaf True -> return 1+    Leaf False -> ifalse <$> get+    Leaf True -> itrue <$> get     Branch v l r -> if l == r then return l else do       s <- get           case VIIM.lookup (v, l, r) ( icore s ) of

@@ -1,7 +1,7 @@ module OBDD.IntIntMap          ( IntIntMap ()       -, empty, lookup, insert, singleton+, empty, lookup, insert, singleton, (!) )           where@@ -21,6 +21,9 @@ lookup (i, j) (IntIntMap mm) = do     m <- M.lookup i mm     M.lookup j m++(!) :: IntIntMap v -> (Int,Int) -> v+IntIntMap m ! (i,j) = m M.! i M.! j  insert (i, j) v (IntIntMap mm) =      case M.lookup i mm of

@@ -1,5 +1,6 @@ {-# language ScopedTypeVariables #-} {-# language PatternGuards #-}+{-# language FlexibleContexts #-}  module OBDD.Operation  @@ -20,26 +21,34 @@ import Ersatz.Bit  import Data.Foldable (toList) +import qualified Data.IntMap as IM+import qualified OBDD.IntIntMap as IIM+import qualified Data.Map as M++import qualified Control.Monad.State.Strict as T+import Control.Monad (forM_) import qualified Data.List ( sortBy) import Data.Function (on)  import Data.Set ( Set ) import qualified Data.Set as S -import Prelude hiding ( (&&), (||), and, or, not, bool )+import Prelude hiding ( (&&), (||), and, or, not, any, all, bool ) import qualified Prelude import qualified Data.Bool  instance Ord v => Boolean (OBDD v) where   bool f = constant f-  not = unary ( Prelude.not )+  not = not_   ( && ) = symmetric_binary ( Prelude.&& )   ( || ) = symmetric_binary ( Prelude.|| )-  choose no yes sel = (no && not sel) || (yes && sel)+  choose no yes sel =+    -- https://github.com/jwaldmann/haskell-obdd/issues/10+    (no && not sel) || (yes && sel)   xor   = symmetric_binary (/=)   ( ==> ) = binary ( <= )-  all p = fold_by_size (constant True ) (&&) . map p . toList-  any p = fold_by_size (constant False) (||) . map p . toList+  all p = fold_by_size true  (&&) . map p . toList+  any p = fold_by_size false (||) . map p . toList  equiv :: Ord v => OBDD v -> OBDD v -> OBDD v equiv = symmetric_binary (==)@@ -57,17 +66,20 @@     in  handle $ Data.List.sortBy (compare `on` size) fs  +-- | FIXME: this function is nonsensical. There is only one interesting+-- unary Boolean function (negation), and it should be handled differently. unary :: Ord v        => ( Bool -> Bool )       -> OBDD v -> OBDD v unary op x = make $ do-    let handle x = cached ( top x, top x ) $ case access x of-                Leaf p -> register $ Leaf $ op p+    let handle x = cachedIM (top x) $ case access x of+                Leaf p -> do+                  T.lift $ register $ Leaf $ op p                 Branch v l r -> do                         l' <- handle l                         r' <- handle r-                        register $ Branch v l' r'-    handle x+                        T.lift $ register $ Branch v l' r'+    flip T.evalStateT IM.empty $ handle x   data Symmetricity = Asymmetric | Symmetric deriving Show@@ -82,36 +94,63 @@       -> 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+-- FIXME https://github.com/jwaldmann/haskell-obdd/issues/4+binary_ _ 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+        handle x y = cachedIIM (top x, top y) $ case ( access x , access y ) of+                    ( Leaf p , Leaf q ) -> do+                        T.lift $ register $ Leaf $ op p q                     ( ax, ay ) -> case comp ax ay of                         LT -> do                             let Branch v l r = ay                             l' <- handle x l                             r' <- handle x r-                            register $ Branch v l' r'+                            T.lift $ register $ Branch v l' r'                         GT -> do                             let Branch v l r = ax                             l' <- handle l y                             r' <- handle r y-                            register $ Branch v l' r'+                            T.lift $ register $ Branch v l' r'                         EQ -> do                             let Branch v1 l1 r1 = ax                                 Branch v2 l2 r2 = ay                                 v = if v1 == v2 then v1 else error "OBDD.Operation.handle"                             l' <- handle l1 l2                             r' <- handle r1 r2-                            register $ Branch v l' r'-    handle x y+                            T.lift $ register $ Branch v l' r'+    flip T.evalStateT IIM.empty $ handle x y++{-# inline cachedM #-}+cachedM arg act = do+  c <- T.get+  case M.lookup arg c of+    Nothing -> do+      res <- act ; T.modify' $ M.insert arg res; return res+    Just res -> do+      return res++{-# inline cachedIM #-}+cachedIM arg act = do+  c <- T.get+  case IM.lookup arg c of+    Nothing -> do+      res <- act ; T.modify' $ IM.insert arg res; return res+    Just res -> do+      return res++{-# inline cachedIIM #-}+cachedIIM arg act = do+  c <- T.get+  case IIM.lookup arg c of+    Nothing -> do+      res <- act ; T.modify' $ IIM.insert arg res; return res+    Just res -> do+      return res  comp x y = case (x , y) of     ( Leaf {} , Leaf {} ) -> EQ