obdd 0.6.1 → 0.8.1

raw patch · 14 files changed

+333/−156 lines, 14 filesdep +ersatzdep +process-extrasdep +textdep −processdep ~basedep ~containersPVP ok

version bump matches the API change (PVP)

Dependencies added: ersatz, process-extras, text

Dependencies removed: process

Dependency ranges changed: base, containers

API changes (from Hackage documentation)

Files

• examples/Cubism.hs +75/−0
• examples/MM0916.hs +4/−5
• examples/Queens.hs +3/−3
• examples/Queens2.hs +2/−2
• examples/Sort.hs +3/−3
• obdd.cabal +10/−4
• src/OBDD.hs +11/−2
• src/OBDD/Cube.hs +94/−0
• src/OBDD/Data.hs +18/−62
• src/OBDD/Display.hs +70/−0
• src/OBDD/Linopt.hs +2/−2
• src/OBDD/Make.hs +1/−7
• src/OBDD/Operation.hs +39/−65
• src/OBDD/Property.hs +1/−1

@@ -0,0 +1,75 @@+{-# LANGUAGE TupleSections #-}+{-# language LambdaCase #-}++import Prelude hiding ((&&),(||),not,and,or)+import OBDD+import OBDD.Cube+import System.Environment (getArgs)++data T = In | L | R | Out   deriving (Eq, Ord, Show)++vars n = (,) <$> [1..n] <*> [L,R,Out]++main = getArgs >>= \ case+ []  -> out $ cnf $ form add 3+ [ "add", s] -> out $ cnf $ form add $ read s+ [ "mul", s] -> out $ cnf $ form mul $ read s+ [ "hist", s] -> out $ cnf $ function (read s) hist+ [ "sort", s] -> out $ cnf $ function (read s) sort+ "king" : cs -> out $ cnf $ constrained_function 9 $ king (map read cs)++out cs = mapM_ (\(k,v) -> putStrLn $ show k ++ " " ++ nice v)+       $ zip [0..] cs++function w f = +  let input = map ( variable . (, In) ) [1 .. w]+      output = map ( variable . (, Out) ) [1 .. ]+  in  and $ zipWith equiv (f input) output++constrained_function w f =+  let input = map ( variable . (, In) ) [1 .. w]+      output = map ( variable . (, Out) ) [1 .. ]+      (c,out) = f input+  in  and $ c : zipWith equiv out output++-- | for MM 12/16+king hs (this : neighbours) =+  let ys = hist neighbours+      cs = map (\ h -> this && ys !! h) hs+  in  ( this ==> or cs , cs )++sort xs =+  let insert ys x =+        zipWith ( \ a b -> a || b && x ) ys ( true : ys )+  in  foldl insert (replicate (length xs) false) xs++-- | histogram xs == ys where  ys !! i <=> exactly i xs,+-- produces a one-hot bit vector.+-- length output = 1 + length input+hist xs =+  let insert ys x =+        zipWith ( \ a b -> choose a b x ) ys ( false : ys )+  in  foldl insert (true : replicate (length xs) false) xs+  +form fun n =+  let make f = ( \ v -> variable (v,f)) <$> [1..n]+      (pre,post) = splitAt n $ fun (make L) (make R)+  in  not (or post) && and ( zipWith equiv pre $ make Out )++mul [] ys = []+mul (x:xs) ys = add (map (&& x) ys) $ false : mul xs ys++add xs ys =+  let go c [] [] = [c]+      go c (x:xs) [] = let (r,d) = halfadd c x in r : go d xs []+      go c [] (y:ys) = let (r,d) = halfadd c y in r : go d ys []+      go c (x:xs) (y:ys) = let (r,d) = fulladd c x y in r : go d xs ys+  in  go false xs ys+      +halfadd x y = (xor x y , x && y)++fulladd x y z =+  let (r , c)  = halfadd x y+      (s , d) = halfadd r z+  in  (s, c || d)+

@@ -64,9 +64,8 @@     $ (  exactly q $ queen <$> positions n )     : ( for ( positions n) $ \ p ->        (not $ queen p) || (not $ attacked p) )-    ++ ( for (positions n) $ \ p -> -     implies (attacked p) $ exactly a $ for directions $ \ d ->-       r A.! (d,p) )+    ++ ( for (positions n) $ \ p ->  attacked p ==>+           ( exactly a $ for directions $ \ d -> r A.! (d,p)))       -- | ray n ! (d,p) == looking in direction d from p,@@ -96,8 +95,8 @@   else exactly_rectangle k xs  exactly_rectangle n xs = last $ -  foldl ( \ cs x -> zipWith ( \ a b -> ite x a b )-                    (false : cs) cs +  foldl ( \ cs x -> zipWith ( \ a b -> choose a b x )+                    cs (false : cs)          ) (true : replicate n false) xs  exactly_direct k xs = atmost k xs && atleast k xs

@@ -13,11 +13,11 @@  import OBDD (OBDD) import qualified OBDD-import qualified OBDD.Data (toDot)  import Control.Monad ( guard ) import System.Environment ( getArgs )-import qualified Data.Set +import qualified Data.Set+import qualified Data.Text.IO as T  type Position = (Int,Int) @@ -74,4 +74,4 @@     m <- OBDD.some_model d     print m -    -- writeFile "Queens.dot" $ OBDD.Data.toDot d+    -- T.writeFile "Queens.dot" $ OBDD.toDot d

@@ -38,12 +38,12 @@  atmostone xs =   let go (n,o) [] = n || o-      go (n,o) (x:xs) = go (bool n false x, bool o n x) xs+      go (n,o) (x:xs) = go (choose n false x, choose 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+      go (n,o) (x:xs) = go (choose n false x, choose o n x) xs   in  go (true,false) xs  handle check f n = OBDD.and $ do

@@ -29,7 +29,7 @@ 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+      go (n,o) (x:xs) = go (choose n false x, choose o n x) xs   in  go (true,false) xs  -- | (weakly) increasing sequence of bits@@ -43,7 +43,7 @@ lt xs ys = or $ zipWith (\x y -> not x && y) xs ys  leq :: Num -> Num -> Bit-leq xs ys = and $ zipWith implies xs ys+leq xs ys = and $ zipWith (==>) xs ys  type Comp = (Int,Int) @@ -86,7 +86,7 @@       f = compat (args s) c && form s   in  s { comps = cs'         , poset = -- mkposet cs'-	    transitive_closure $ S.insert c $ poset s+            transitive_closure $ S.insert c $ poset s         , form = f         , size = number_of_models (vars w) f         }

@@ -1,5 +1,5 @@ Name:                obdd-Version:             0.6.1+Version:             0.8.1 Cabal-Version:       >= 1.8 Build-type: Simple Synopsis:            Ordered Reduced Binary Decision Diagrams@@ -38,9 +38,9 @@     Location: git://github.com/jwaldmann/haskell-obdd.git  Library-    Build-Depends:       base==4.*, random, mtl, containers>=0.5, array, process+    Build-Depends:       base==4.*, random, mtl, containers>=0.5, array, process-extras, ersatz, text     Hs-Source-Dirs:	     src-    Exposed-Modules:     OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property, OBDD.Linopt+    Exposed-Modules:     OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property, OBDD.Display, OBDD.Linopt, OBDD.Cube     Other-Modules:	     OBDD.IntIntMap, OBDD.VarIntIntMap     ghc-options: -funbox-strict-fields @@ -50,12 +50,18 @@     Main-Is: Placement.hs     Build-Depends: base, containers, obdd +test-suite obdd-cubism+    Hs-Source-Dirs : examples+    Type: exitcode-stdio-1.0+    Main-Is: Cubism.hs+    Build-Depends: base, containers, obdd+ test-suite obdd-queens     Hs-Source-Dirs : examples     Type: exitcode-stdio-1.0     Main-Is: Queens.hs     ghc-options: -threaded -rtsopts-    Build-Depends: base, containers, obdd+    Build-Depends: base, containers, obdd, text  test-suite obdd-queens2     Hs-Source-Dirs : examples

@@ -7,15 +7,24 @@  module OBDD  -( OBDD, display+( module OBDD.Data , module OBDD.Property , module OBDD.Operation+, module OBDD.Display , module OBDD.Make )   where -import OBDD.Data ( OBDD, display )+import OBDD.Data ( OBDD , size+                 , null, satisfiable+                 , number_of_models+                 , variables, paths, models+                 , some_model+                 , fold, foldM+                 , full_fold, full_foldM+                 ) import OBDD.Property import OBDD.Operation+import OBDD.Display import OBDD.Make

@@ -0,0 +1,94 @@+{-# language FlexibleContexts #-}+{-# LANGUAGE TupleSections #-}++module OBDD.Cube where++import Prelude hiding ((&&),(||),not,and,or)+import qualified Prelude+import OBDD++import qualified Data.Bool +import Control.Monad (guard)+import Control.Applicative++import qualified Data.Map.Strict as M+import qualified Data.Set as S+import Data.List (partition, sortOn)++import Debug.Trace++type Cube v = M.Map v Bool++primes :: Ord v => OBDD v -> [Cube v]+primes d =+  let process m = M.fromList $ do+        ((v,Sign), b) <- M.toList m+        return (v, b)+  in map process $ paths $ prime d++nice :: Show v => Cube v -> String+nice c = "(" ++ do+    (v,b) <- M.toList c+    (if b then " " else " -") ++ show v+  ++ ")"++data Check = Sign | Occurs | Original+           deriving (Eq, Ord, Show)++sign v = variable (v, Sign)+occurs v = variable (v, Occurs)+original v = variable (v, Original)++process c = M.fromList $ do+        ((v,Occurs),True) <- M.toList c+        return (v, c M.! (v,Sign))+++-- | O. Coudert , J. C. Madre:+-- http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.3330++prime :: Ord v => OBDD v -> OBDD (v, Check)+prime = snd+  . fold ( \ b -> ( bool b, bool b ))+         ( \ v (fl,pl) (fr,pr) -> ( choose fl fr (variable v)+               , let common = prime (fl && fr)+                 in      not (occurs v) && common+                     || occurs v && not (sign v) && pl && not common+                     || occurs v &&     (sign v) && pr && not common+               )+         )+++-- * naive way of finding a minimal set of clauses.++dnf f =+  let ps = primes f+      ms = models (variables f) f+      covering = do+        m <- ms+        return $ S.fromList $ do+                   (i,p) <- zip [0..] ps+                   guard $ M.isSubmapOf p m+                   return i+      cost = M.fromList $ zip [0..] $ map M.size ps+      r = greed cost covering+  in  map (ps !!) $ S.toList r+++cnf f = map (M.map Prelude.not) $ dnf $ not f++greed cost [] = S.empty+greed cost could =+  let count = M.unionsWith (+) $ do+        c <- could+        return $ M.fromList $ zip (S.toList c) $ repeat 1+      this = fst+           $ head+           $ sortOn snd+           $ map (\(k,v) -> (k, (negate v, cost M.! k)))+           $ M.toList count +  in    S.insert this+      $ greed cost $ filter ( \p -> S.notMember this p ) could++clause c = and $ do (v,b) <- M.toList c ; return $ unit v b+

@@ -14,10 +14,10 @@ -- * for external use , null, satisfiable , number_of_models-, some_model, all_models+, variables, paths, models+, some_model , fold, foldM , full_fold, full_foldM-, toDot, display -- * for internal use , Node (..) , make@@ -55,7 +55,6 @@ import Control.Monad ( forM, guard, void ) import qualified Control.Monad ( foldM ) import Data.Functor.Identity-import System.Process import Data.List (isPrefixOf, isSuffixOf)  import Prelude hiding ( null )@@ -143,7 +142,7 @@      -> ( v -> a -> a -> m a )      -> OBDD v -> m a full_foldM vars leaf branch o = do-    let vs = S.toAscList vars+    let vs = S.toAscList $ S.union (variables o) vars         low = head vs         m = M.fromList $ zip vs $ tail vs         up v = M.lookup v m@@ -225,14 +224,25 @@         Just m <- some_model t         return $ Just $ M.insert v p m  --- | list of all models (WARNING not using --- variables that had been deleted)-all_models :: Ord v => OBDD v -> [ Map v Bool ]-all_models = +-- | all variables that occur in the nodes+variables :: Ord v => OBDD v -> S.Set v+variables f = fold (\ b ->  S.empty )+         ( \ v l r -> S.insert v $ S.union l r ) f++-- | list of all paths+paths :: Ord v => OBDD v -> [ Map v Bool ]+paths =    fold ( bool [] [ M.empty ] )        ( \ v l r -> (M.insert v False <$> l)                  ++ (M.insert v True  <$> r) ) +-- | list of all models (a.k.a. minterms)+models vars =+  full_fold vars ( bool [] [ M.empty ] )+       ( \ v l r -> (M.insert v False <$> l)+                 ++ (M.insert v True  <$> r) )+  + select_one :: [a] -> IO a select_one xs | not ( Prelude.null xs ) = do     i <- System.Random.randomRIO ( 0, length xs - 1 )@@ -299,57 +309,3 @@       check_var_ordering l ; check_var_ordering r       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.-toDot :: (Show v) => OBDD v -> String-toDot (OBDD idmap _ _ top _) =-    unlines [ "digraph BDD {"-            -- Start in oval mode-            , "node[shape=oval];"-            , evalState (helper $ idToNode top) S.empty-            , "}"-            ]-  where-    idToNode =-        let getNode = \i -> case i of-                          0 -> Leaf False-                          1 -> Leaf True-                          _ -> idmap IM.! i-        in id &&& getNode--    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.-        unlines [ "node[shape=rectangle];"-                , show thisId ++ mkLabel (show b)-                , "node[shape=oval];"-                ]-    helper (thisId, Branch vid l r) = do-        -- Ensure we don't traverse children multiple times, if we have more-        -- than one edge into a given node.-        beenHere <- gets (thisId `S.member`)-        if beenHere-            then return ""-            else do-                lstr <- helper $ idToNode l-                rstr <- helper $ idToNode r-                modify (thisId `S.insert`)-                let idStr = show thisId-                return $ unlines-                   [ idStr ++ mkLabel (show vid)-                   , lstr-                   , idStr ++ "->" ++ show l ++ mkLabel "0"-                   , rstr-                   , idStr ++ "->" ++ show r ++ mkLabel "1"-                   ]

@@ -0,0 +1,70 @@+{-# language OverloadedStrings #-}++module OBDD.Display where++import OBDD.Data (OBDD, foldM)+import Control.Monad (void)+import Control.Monad.RWS (RWS, evalRWS, tell, get, put)+import Data.Text (Text)+import qualified Data.Text as T+import Data.Monoid+import System.Process.Text++-- | 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 :: (Ord v, Show v) => OBDD v -> IO ()+display d = void+  $ readProcessWithExitCode "dot" [ "-Tx11" ]+  $ toDot False d++-- | same as @display@, but does not show the @False@ node+-- and the edges pointing to @False@.+display' :: (Ord v, Show v) => OBDD v -> IO ()+display' d = void+  $ readProcessWithExitCode "dot" [ "-Tx11" ]+  $ toDot True d++-- | a textual representation of the BDD that is suitable+-- as input to the "dot" program from the graphviz suite.+toDot :: (Ord v, Show v)+  => Bool -- ^ suppress pointers to False+  -> OBDD v -> Text+toDot suppress_false =+    snd+  . ( \ m -> evalRWS (do tell "digraph BDD {"; m; tell "}" ) () 0 )+  . foldM+  ( \ b -> if not b && suppress_false then return Nothing else do+     this <- fresh+     tell $ T.unlines+       [ "node[shape=rectangle];"+       , text this <> mkLabel (text b)+       , "node[shape=oval];"+       ]+     return $ Just this+  )+  ( \ v ml mr -> do+     this <- fresh+     tell $ text this <> mkLabel (text v)+     case ml of+       Just l -> tell $ text this <> "->" <> text l <> mkLabel "0"+       Nothing -> return ()+     case mr of+       Just r -> tell $ text this <> "->" <> text r <> mkLabel "1"+       Nothing -> return ()+     return $ Just this+  )++fresh :: Monoid b => RWS a b Int Int+fresh = do this <- get ; put $! succ this ; return this++mkLabel lbl = "[label=\"" <> unquote lbl <> "\"];"++unquote s =+  if T.isPrefixOf "\"" s && T.isSuffixOf "\"" s+  then T.init $ T.tail s+  else s++text x = T.pack $ show x

@@ -8,8 +8,8 @@ -- | solve the constrained linear optimisation problem: -- returns an assignment that is a model of the BDD -- and maximises the sum of weights of variables.--- The set of keys of the weight map *must* be the--- full set of variables.+-- Keys missing from the weight map, but present in the BDD,+-- get weight zero. linopt :: ( Ord v , Num w, Ord w )         => OBDD v         -> M.Map v w 

@@ -2,7 +2,7 @@  module OBDD.Make  -( constant, unit, variable, false, true )+( constant, unit, variable )  where @@ -14,12 +14,6 @@ constant :: Ord v => Bool -> OBDD v 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

@@ -3,11 +3,12 @@  module OBDD.Operation  -( (&&), (||), not, and, or-, ite, bool, implies, equiv, xor+( Boolean(..)+, equiv , unary, binary , instantiate , exists, exists_many+, forall, forall_many , fold, foldM , full_fold, full_foldM )@@ -16,6 +17,8 @@  import OBDD.Data import OBDD.Make+import Ersatz.Bit +import Data.Foldable (toList)  import qualified Data.List ( sortBy) import Data.Function (on)@@ -23,47 +26,24 @@ import Data.Set ( Set ) import qualified Data.Set as S --- import Data.List ( foldl' )--- don't use, see below- import Prelude hiding ( (&&), (||), and, or, not, bool ) import qualified Prelude--infixr 3 &&--( && ) :: Ord v => OBDD v -> OBDD v -> OBDD v-( && ) = symmetric_binary ( Prelude.&& )--infixr 2 ||--( || ) :: Ord v => OBDD v -> OBDD v -> OBDD v-( || ) = symmetric_binary ( Prelude.|| )--bool :: Ord v => OBDD v -> OBDD v -> OBDD v -> OBDD v-bool f t p = (f && not p) || (t && p)+import qualified Data.Bool -ite :: Ord v => OBDD v -> OBDD v -> OBDD v -> OBDD v-ite i t e = bool e t i+instance Ord v => Boolean (OBDD v) where+  bool f = constant f+  not = unary ( Prelude.not )+  ( && ) = symmetric_binary ( Prelude.&& )+  ( || ) = symmetric_binary ( Prelude.|| )+  choose no yes sel = (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  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 ) --- writing foldl or fold' here --- makes performance MUCH worse!--or :: Ord v => [ OBDD v ] -> OBDD v-or = fold_by_size (constant False) (||)--- or = foldr ( || ) ( constant False ) - fold_by_size base reduce fs =     let handle fs = case fs of             [] -> base@@ -77,11 +57,6 @@     in  handle $ Data.List.sortBy (compare `on` size) fs  --- | FIXME this is a silly implementation. Negation should be done--- by switching values in Leaves (?)-not :: Ord v => OBDD v -> OBDD v -not = unary ( Prelude.not )- unary :: Ord v        => ( Bool -> Bool )       -> OBDD v -> OBDD v@@ -138,44 +113,43 @@                             register $ Branch v l' r'     handle x y +comp x y = case (x , y) of+    ( Leaf {} , Leaf {} ) -> EQ+    ( Branch {} , Leaf {} ) -> GT+    ( Leaf {} , Branch {} ) ->  LT+    ( Branch v1 _ _ , Branch v2 _ _ ) -> compare v1 v2+ -- | remove variables existentially--- TODO: needs better implementation-exists_many :: Ord v -            => Set v+exists_many :: (Foldable c, Ord v)+            => c v             -> OBDD v             -> OBDD v exists_many vars x =-    foldr exists x $ S.toList vars +    foldr exists x vars   -- | remove variable existentially--- TODO: needs better implementation exists :: Ord v       => v       -> OBDD v -> OBDD v-exists var x = -    instantiate var False x || instantiate var True x+exists var = fold bool+  ( \ v l r -> if var == v then l || r else choose l r (variable v) ) +forall_many :: (Foldable c, Ord v) => c v -> OBDD v -> OBDD v+forall_many vars x = +    foldr forall x vars ++forall :: Ord v => v -> OBDD v -> OBDD v+forall var = fold bool+  ( \ v l r -> if var == v then l && r else choose l r (variable v) )+ -- | replace variable by value instantiate :: Ord v =>              v -> Bool              -> OBDD v             -> OBDD v-instantiate var val x = make $ do-    let handle x = cached ( top x, top x ) $ case access x of-            Leaf p -> register $ Leaf p-            Branch v l r -> -                if v == var then do-                     let t = if val then r else l-                     handle t-                else  do-                     l' <- handle l-                     r' <- handle r-                     register $ Branch v l' r' -    handle x+instantiate var val = fold bool+  ( \ v l r ->+    if var == v then Data.Bool.bool l r val+    else choose l r (variable v) ) -comp x y = case (x , y) of-    ( Leaf {} , Leaf {} ) -> EQ-    ( Branch {} , Leaf {} ) -> GT-    ( Leaf {} , Branch {} ) ->  LT-    ( Branch v1 _ _ , Branch v2 _ _ ) -> compare v1 v2     

@@ -2,7 +2,7 @@  ( null, satisfiable , number_of_models-, some_model, all_models+, paths, models , size )