Skip to content

Commit

Permalink
Merge 8e1089a into 2cb4a1b
Browse files Browse the repository at this point in the history
  • Loading branch information
msakai committed Nov 23, 2021
2 parents 2cb4a1b + 8e1089a commit 63573c6
Show file tree
Hide file tree
Showing 3 changed files with 59 additions and 66 deletions.
36 changes: 3 additions & 33 deletions src/Data/DecisionDiagram/BDD.hs
Expand Up @@ -125,7 +125,6 @@ import Control.Monad.ST.Unsafe
import Data.Bits (Bits (shiftL))
import qualified Data.Foldable as Foldable
import Data.Function (on)
import Data.Functor.Identity
import Data.Hashable
import qualified Data.HashMap.Lazy as HashMap
import qualified Data.HashTable.Class as H
Expand All @@ -139,7 +138,6 @@ import Data.Map.Lazy (Map)
import qualified Data.Map.Lazy as Map
import Data.Proxy
import Data.Ratio
import Data.STRef
import qualified Data.Vector as V
import Numeric.Natural
#if MIN_VERSION_mwc_random(0,15,0)
Expand All @@ -152,7 +150,7 @@ import System.Random.MWC.Distributions (bernoulli)
import Text.Read

import Data.DecisionDiagram.BDD.Internal.ItemOrder
import Data.DecisionDiagram.BDD.Internal.Node (Sig (..))
import Data.DecisionDiagram.BDD.Internal.Node (Sig (..), Graph)
import qualified Data.DecisionDiagram.BDD.Internal.Node as Node

infixr 3 .&&.
Expand Down Expand Up @@ -1050,45 +1048,17 @@ outSig (Branch x lo hi) = SBranch x lo hi

-- ------------------------------------------------------------------------

type Graph f = IntMap (f Int)

-- | Convert a BDD into a pointed graph
--
-- Nodes @0@ and @1@ are reserved for @SLeaf False@ and @SLeaf True@
-- even if they are not actually used. Therefore the result may be
-- larger than 'numNodes' if the leaf nodes are not used.
toGraph :: BDD a -> (Graph Sig, Int)
toGraph bdd =
case toGraph' (Identity bdd) of
(g, Identity v) -> (g, v)
toGraph (BDD node) = Node.toGraph node

-- | Convert multiple BDDs into a graph
toGraph' :: Traversable t => t (BDD a) -> (Graph Sig, t Int)
toGraph' bs = runST $ do
h <- C.newSized defaultTableSize
H.insert h F 0
H.insert h T 1
counter <- newSTRef 2
ref <- newSTRef $ IntMap.fromList [(0, SLeaf False), (1, SLeaf True)]

let f F = return 0
f T = return 1
f p@(Branch x lo hi) = do
m <- H.lookup h p
case m of
Just ret -> return ret
Nothing -> do
r0 <- f lo
r1 <- f hi
n <- readSTRef counter
writeSTRef counter $! n+1
H.insert h p n
modifySTRef' ref (IntMap.insert n (SBranch x r0 r1))
return n

vs <- mapM f bs
g <- readSTRef ref
return (g, vs)
toGraph' bs = Node.toGraph' (fmap (\(BDD node) -> node) bs)

-- | Convert a pointed graph into a BDD
fromGraph :: (Graph Sig, Int) -> BDD a
Expand Down
53 changes: 53 additions & 0 deletions src/Data/DecisionDiagram/BDD/Internal/Node.hs
Expand Up @@ -35,15 +35,24 @@ module Data.DecisionDiagram.BDD.Internal.Node

-- * (Co)algebraic structure
, Sig (..)

-- * Graph
, Graph
, toGraph
, toGraph'
) where

import Control.Monad
import Control.Monad.ST
import Control.Monad.ST.Unsafe
import Data.Functor.Identity
import Data.Hashable
import qualified Data.HashTable.Class as H
import qualified Data.HashTable.ST.Cuckoo as C
import Data.Interned
import Data.IntMap.Lazy (IntMap)
import qualified Data.IntMap.Lazy as IntMap
import Data.STRef
import GHC.Generics

-- ------------------------------------------------------------------------
Expand Down Expand Up @@ -192,3 +201,47 @@ mkFold'Op br lf = do

-- ------------------------------------------------------------------------

-- | Graph where nodes are decorated using a functor @f@.
--
-- The occurrences of the parameter of @f@ represent out-going edges.
type Graph f = IntMap (f Int)

-- | Convert a node into a pointed graph
--
-- Nodes @0@ and @1@ are reserved for @SLeaf False@ and @SLeaf True@ even if
-- they are not actually used. Therefore the result may be larger than
-- 'numNodes' if the leaf nodes are not used.
toGraph :: Node -> (Graph Sig, Int)
toGraph bdd =
case toGraph' (Identity bdd) of
(g, Identity v) -> (g, v)

-- | Convert multiple nodes into a graph
toGraph' :: Traversable t => t Node -> (Graph Sig, t Int)
toGraph' bs = runST $ do
h <- C.newSized defaultTableSize
H.insert h (Leaf False) 0
H.insert h (Leaf True) 1
counter <- newSTRef 2
ref <- newSTRef $ IntMap.fromList [(0, SLeaf False), (1, SLeaf True)]

let f (Leaf False) = return 0
f (Leaf True) = return 1
f p@(Branch x lo hi) = do
m <- H.lookup h p
case m of
Just ret -> return ret
Nothing -> do
r0 <- f lo
r1 <- f hi
n <- readSTRef counter
writeSTRef counter $! n+1
H.insert h p n
modifySTRef' ref (IntMap.insert n (SBranch x r0 r1))
return n

vs <- mapM f bs
g <- readSTRef ref
return (g, vs)

-- ------------------------------------------------------------------------
36 changes: 3 additions & 33 deletions src/Data/DecisionDiagram/ZDD.hs
Expand Up @@ -143,7 +143,6 @@ import Control.Monad.Primitive
import Control.Monad.ST
import qualified Data.Foldable as Foldable
import Data.Function (on)
import Data.Functor.Identity
import Data.Hashable
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as HashMap
Expand All @@ -161,7 +160,6 @@ import Data.Proxy
import Data.Ratio
import Data.Set (Set)
import qualified Data.Set as Set
import Data.STRef
import qualified Data.Vector as V
import qualified GHC.Exts as Exts
import Numeric.Natural
Expand All @@ -174,7 +172,7 @@ import System.Random.MWC.Distributions (bernoulli)
import Text.Read

import Data.DecisionDiagram.BDD.Internal.ItemOrder
import Data.DecisionDiagram.BDD.Internal.Node (Sig (..))
import Data.DecisionDiagram.BDD.Internal.Node (Sig (..), Graph)
import qualified Data.DecisionDiagram.BDD.Internal.Node as Node
import qualified Data.DecisionDiagram.BDD as BDD

Expand Down Expand Up @@ -1002,45 +1000,17 @@ outSig (Branch x lo hi) = SBranch x lo hi

-- ------------------------------------------------------------------------

type Graph f = IntMap (f Int)

-- | Convert a ZDD into a pointed graph
--
-- Nodes @0@ and @1@ are reserved for @SLeaf False@ and @SLeaf True@ even if
-- they are not actually used. Therefore the result may be larger than
-- 'numNodes' if the leaf nodes are not used.
toGraph :: ZDD a -> (Graph Sig, Int)
toGraph bdd =
case toGraph' (Identity bdd) of
(g, Identity v) -> (g, v)
toGraph (ZDD node) = Node.toGraph node

-- | Convert multiple ZDDs into a graph
toGraph' :: Traversable t => t (ZDD a) -> (Graph Sig, t Int)
toGraph' bs = runST $ do
h <- C.newSized defaultTableSize
H.insert h Empty 0
H.insert h Base 1
counter <- newSTRef 2
ref <- newSTRef $ IntMap.fromList [(0, SLeaf False), (1, SLeaf True)]

let f Empty = return 0
f Base = return 1
f p@(Branch x lo hi) = do
m <- H.lookup h p
case m of
Just ret -> return ret
Nothing -> do
r0 <- f lo
r1 <- f hi
n <- readSTRef counter
writeSTRef counter $! n+1
H.insert h p n
modifySTRef' ref (IntMap.insert n (SBranch x r0 r1))
return n

vs <- mapM f bs
g <- readSTRef ref
return (g, vs)
toGraph' bs = Node.toGraph' (fmap (\(ZDD node) -> node) bs)

-- | Convert a pointed graph into a ZDD
fromGraph :: (Graph Sig, Int) -> ZDD a
Expand Down

0 comments on commit 63573c6

Please sign in to comment.