{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
----------------------------------------------------------------------
-- |
-- Module      :  Data.DecisionDiagram.ZDD
-- Copyright   :  (c) Masahiro Sakai 2021
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  unstable
-- Portability :  non-portable
--
-- Zero-Suppressed binary decision diagram.
--
-- References:
--
-- * S. Minato, "Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems,"
--   30th ACM/IEEE Design Automation Conference, 1993, pp. 272-277,
--   doi: [10.1145/157485.164890](https://doi.org/10.1145/157485.164890).
--   <https://www.researchgate.net/publication/221062015_Zero-Suppressed_BDDs_for_Set_Manipulation_in_Combinatorial_Problems>
--
----------------------------------------------------------------------
module Data.DecisionDiagram.ZDD
  (
  -- * ZDD type
    ZDD (Empty, Base, Branch)

  -- * Item ordering
  , ItemOrder (..)
  , AscOrder
  , DescOrder
  , withDefaultOrder
  , withAscOrder
  , withDescOrder
  , withCustomOrder

  -- * Construction
  , empty
  , base
  , singleton
  , subsets
  , fromListOfIntSets
  , fromSetOfIntSets

  -- * Insertion
  , insert

  -- * Deletion
  , delete

  -- * Query
  , member
  , notMember
  , null
  , size
  , isSubsetOf
  , isProperSubsetOf
  , disjoint

  -- * Combine
  , union
  , unions
  , intersection
  , difference
  , (\\)
  , nonSuperset

  -- * Filter
  , subset1
  , subset0

  -- * Map
  , mapInsert
  , mapDelete
  , change

  -- * Fold
  , fold
  , fold'

  -- * Minimal hitting sets
  , minimalHittingSets
  , minimalHittingSetsToda
  , minimalHittingSetsKnuth
  , minimalHittingSetsImai

  -- * Random sampling
  , uniformM

  -- * Min/Max
  , findMinSum
  , findMaxSum

  -- * Misc
  , flatten

  -- * Conversion
  , toListOfIntSets
  , toSetOfIntSets

  -- ** Conversion from/to graphs
  , Graph
  , Node (..)
  , toGraph
  , toGraph'
  , fromGraph
  , fromGraph'
  ) where

import Prelude hiding (null)

import Control.Monad
#if !MIN_VERSION_mwc_random(0,15,0)
import Control.Monad.Primitive
#endif
import Control.Monad.ST
import Data.Functor.Identity
import Data.Hashable
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as HashMap
import qualified Data.HashTable.Class as H
import qualified Data.HashTable.ST.Cuckoo as C
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.List (foldl', sortBy)
import Data.Maybe
import Data.Proxy
import Data.Ratio
import Data.Set (Set)
import qualified Data.Set as Set
import Data.STRef
import qualified GHC.Exts as Exts
import Numeric.Natural
#if MIN_VERSION_mwc_random(0,15,0)
import System.Random.Stateful (StatefulGen (..))
#else
import System.Random.MWC (Gen)
#endif
import System.Random.MWC.Distributions (bernoulli)
import Text.Read

import Data.DecisionDiagram.BDD.Internal.ItemOrder
import qualified Data.DecisionDiagram.BDD.Internal.Node as Node
import qualified Data.DecisionDiagram.BDD as BDD

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

defaultTableSize :: Int
defaultTableSize :: Int
defaultTableSize = Int
256

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

-- | Zero-suppressed binary decision diagram representing family of sets
newtype ZDD a = ZDD Node.Node
  deriving (ZDD a -> ZDD a -> Bool
(ZDD a -> ZDD a -> Bool) -> (ZDD a -> ZDD a -> Bool) -> Eq (ZDD a)
forall a. ZDD a -> ZDD a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ZDD a -> ZDD a -> Bool
$c/= :: forall a. ZDD a -> ZDD a -> Bool
== :: ZDD a -> ZDD a -> Bool
$c== :: forall a. ZDD a -> ZDD a -> Bool
Eq, Int -> ZDD a -> Int
ZDD a -> Int
(Int -> ZDD a -> Int) -> (ZDD a -> Int) -> Hashable (ZDD a)
forall a. Int -> ZDD a -> Int
forall a. ZDD a -> Int
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: ZDD a -> Int
$chash :: forall a. ZDD a -> Int
hashWithSalt :: Int -> ZDD a -> Int
$chashWithSalt :: forall a. Int -> ZDD a -> Int
Hashable)

pattern Empty :: ZDD a
pattern $bEmpty :: ZDD a
$mEmpty :: forall r a. ZDD a -> (Void# -> r) -> (Void# -> r) -> r
Empty = ZDD Node.F

pattern Base :: ZDD a
pattern $bBase :: ZDD a
$mBase :: forall r a. ZDD a -> (Void# -> r) -> (Void# -> r) -> r
Base = ZDD Node.T

-- | Smart constructor that takes the ZDD reduction rules into account
pattern Branch :: Int -> ZDD a -> ZDD a -> ZDD a
pattern $bBranch :: Int -> ZDD a -> ZDD a -> ZDD a
$mBranch :: forall r a.
ZDD a -> (Int -> ZDD a -> ZDD a -> r) -> (Void# -> r) -> r
Branch x lo hi <- ZDD (Node.Branch x (ZDD -> lo) (ZDD -> hi)) where
  Branch Int
_ ZDD a
p0 ZDD a
Empty = ZDD a
p0
  Branch Int
x (ZDD Node
lo) (ZDD Node
hi) = Node -> ZDD a
forall a. Node -> ZDD a
ZDD (Int -> Node -> Node -> Node
Node.Branch Int
x Node
lo Node
hi)

{-# COMPLETE Empty, Base, Branch #-}

nodeId :: ZDD a -> Int
nodeId :: ZDD a -> Int
nodeId (ZDD Node
node) = Node -> Int
Node.nodeId Node
node

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

instance Show (ZDD a) where
  showsPrec :: Int -> ZDD a -> ShowS
showsPrec Int
d ZDD a
a   = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"fromGraph " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Graph, Int) -> ShowS
forall a. Show a => a -> ShowS
shows (ZDD a -> (Graph, Int)
forall a. ZDD a -> (Graph, Int)
toGraph ZDD a
a)

instance Read (ZDD a) where
  readPrec :: ReadPrec (ZDD a)
readPrec = ReadPrec (ZDD a) -> ReadPrec (ZDD a)
forall a. ReadPrec a -> ReadPrec a
parens (ReadPrec (ZDD a) -> ReadPrec (ZDD a))
-> ReadPrec (ZDD a) -> ReadPrec (ZDD a)
forall a b. (a -> b) -> a -> b
$ Int -> ReadPrec (ZDD a) -> ReadPrec (ZDD a)
forall a. Int -> ReadPrec a -> ReadPrec a
prec Int
10 (ReadPrec (ZDD a) -> ReadPrec (ZDD a))
-> ReadPrec (ZDD a) -> ReadPrec (ZDD a)
forall a b. (a -> b) -> a -> b
$ do
    Ident String
"fromGraph" <- ReadPrec Lexeme
lexP
    (Graph, Int)
gv <- ReadPrec (Graph, Int)
forall a. Read a => ReadPrec a
readPrec
    ZDD a -> ReadPrec (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Graph, Int) -> ZDD a
forall a. (Graph, Int) -> ZDD a
fromGraph (Graph, Int)
gv)

  readListPrec :: ReadPrec [ZDD a]
readListPrec = ReadPrec [ZDD a]
forall a. Read a => ReadPrec [a]
readListPrecDefault

instance ItemOrder a => Exts.IsList (ZDD a) where
  type Item (ZDD a) = IntSet

  fromList :: [Item (ZDD a)] -> ZDD a
fromList = [[Int]] -> ZDD a
forall a. ItemOrder a => [[Int]] -> ZDD a
fromListOfSortedList ([[Int]] -> ZDD a) -> ([IntSet] -> [[Int]]) -> [IntSet] -> ZDD a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntSet -> [Int]) -> [IntSet] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map IntSet -> [Int]
f
    where
      f :: IntSet -> [Int]
      f :: IntSet -> [Int]
f = (Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) ([Int] -> [Int]) -> (IntSet -> [Int]) -> IntSet -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IntSet.toList

  toList :: ZDD a -> [Item (ZDD a)]
toList = [IntSet]
-> [IntSet]
-> (Int -> [IntSet] -> [IntSet] -> [IntSet])
-> ZDD a
-> [IntSet]
forall b a. b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
fold' [] [IntSet
IntSet.empty] (\Int
top [IntSet]
lo [IntSet]
hi -> [IntSet]
lo [IntSet] -> [IntSet] -> [IntSet]
forall a. Semigroup a => a -> a -> a
<> (IntSet -> IntSet) -> [IntSet] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> IntSet -> IntSet
IntSet.insert Int
top) [IntSet]
hi)

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

data ZDDCase2 a
  = ZDDCase2LT Int (ZDD a) (ZDD a)
  | ZDDCase2GT Int (ZDD a) (ZDD a)
  | ZDDCase2EQ Int (ZDD a) (ZDD a) (ZDD a) (ZDD a)
  | ZDDCase2EQ2 Bool Bool

zddCase2 :: forall a. ItemOrder a => Proxy a -> ZDD a -> ZDD a -> ZDDCase2 a
zddCase2 :: Proxy a -> ZDD a -> ZDD a -> ZDDCase2 a
zddCase2 Proxy a
_ (Branch Int
ptop ZDD a
p0 ZDD a
p1) (Branch Int
qtop ZDD a
q0 ZDD a
q1) =
  case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
ptop Int
qtop of
    Ordering
LT -> Int -> ZDD a -> ZDD a -> ZDDCase2 a
forall a. Int -> ZDD a -> ZDD a -> ZDDCase2 a
ZDDCase2LT Int
ptop ZDD a
p0 ZDD a
p1
    Ordering
GT -> Int -> ZDD a -> ZDD a -> ZDDCase2 a
forall a. Int -> ZDD a -> ZDD a -> ZDDCase2 a
ZDDCase2GT Int
qtop ZDD a
q0 ZDD a
q1
    Ordering
EQ -> Int -> ZDD a -> ZDD a -> ZDD a -> ZDD a -> ZDDCase2 a
forall a. Int -> ZDD a -> ZDD a -> ZDD a -> ZDD a -> ZDDCase2 a
ZDDCase2EQ Int
ptop ZDD a
p0 ZDD a
p1 ZDD a
q0 ZDD a
q1
zddCase2 Proxy a
_ (Branch Int
ptop ZDD a
p0 ZDD a
p1) ZDD a
_ = Int -> ZDD a -> ZDD a -> ZDDCase2 a
forall a. Int -> ZDD a -> ZDD a -> ZDDCase2 a
ZDDCase2LT Int
ptop ZDD a
p0 ZDD a
p1
zddCase2 Proxy a
_ ZDD a
_ (Branch Int
qtop ZDD a
q0 ZDD a
q1) = Int -> ZDD a -> ZDD a -> ZDDCase2 a
forall a. Int -> ZDD a -> ZDD a -> ZDDCase2 a
ZDDCase2GT Int
qtop ZDD a
q0 ZDD a
q1
zddCase2 Proxy a
_ ZDD a
Base ZDD a
Base = Bool -> Bool -> ZDDCase2 a
forall a. Bool -> Bool -> ZDDCase2 a
ZDDCase2EQ2 Bool
True Bool
True
zddCase2 Proxy a
_ ZDD a
Base ZDD a
Empty = Bool -> Bool -> ZDDCase2 a
forall a. Bool -> Bool -> ZDDCase2 a
ZDDCase2EQ2 Bool
True Bool
False
zddCase2 Proxy a
_ ZDD a
Empty ZDD a
Base = Bool -> Bool -> ZDDCase2 a
forall a. Bool -> Bool -> ZDDCase2 a
ZDDCase2EQ2 Bool
False Bool
True
zddCase2 Proxy a
_ ZDD a
Empty ZDD a
Empty = Bool -> Bool -> ZDDCase2 a
forall a. Bool -> Bool -> ZDDCase2 a
ZDDCase2EQ2 Bool
False Bool
False

-- | The empty set (∅).
empty :: ZDD a
empty :: ZDD a
empty = ZDD a
forall a. ZDD a
Empty

-- | The set containing only the empty set ({∅}).
base :: ZDD a
base :: ZDD a
base = ZDD a
forall a. ZDD a
Base

-- | Create a ZDD that contains only a given set.
singleton :: forall a. ItemOrder a => IntSet -> ZDD a
singleton :: IntSet -> ZDD a
singleton IntSet
xs = IntSet -> ZDD a -> ZDD a
forall a. ItemOrder a => IntSet -> ZDD a -> ZDD a
insert IntSet
xs ZDD a
forall a. ZDD a
empty

-- | Set of all subsets, i.e. powerset
subsets :: forall a. ItemOrder a => IntSet -> ZDD a
subsets :: IntSet -> ZDD a
subsets = (ZDD a -> Int -> ZDD a) -> ZDD a -> [Int] -> ZDD a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ZDD a -> Int -> ZDD a
forall a. ZDD a -> Int -> ZDD a
f ZDD a
forall a. ZDD a
Base ([Int] -> ZDD a) -> (IntSet -> [Int]) -> IntSet -> ZDD a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Int -> Int -> Ordering) -> Int -> Int -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a))) ([Int] -> [Int]) -> (IntSet -> [Int]) -> IntSet -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IntSet.toList
  where
    f :: ZDD a -> Int -> ZDD a
f ZDD a
zdd Int
x = Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
x ZDD a
zdd ZDD a
zdd

-- | Select subsets that contain a particular element and then remove the element from them
subset1 :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a
subset1 :: Int -> ZDD a -> ZDD a
subset1 Int
var ZDD a
zdd = (forall s. ST s (ZDD a)) -> ZDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (ZDD a)) -> ZDD a)
-> (forall s. ST s (ZDD a)) -> ZDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (ZDD a) (ZDD a)
h <- Int -> ST s (HashTable s (ZDD a) (ZDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: ZDD a -> ST s (ZDD a)
f ZDD a
Base = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f ZDD a
Empty = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f p :: ZDD a
p@(Branch Int
top ZDD a
p0 ZDD a
p1) = do
        Maybe (ZDD a)
m <- HashTable s (ZDD a) (ZDD a) -> ZDD a -> ST s (Maybe (ZDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a) (ZDD a)
h ZDD a
p
        case Maybe (ZDD a)
m of
          Just ZDD a
ret -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
          Maybe (ZDD a)
Nothing -> do
            ZDD a
ret <- case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
top Int
var of
              Ordering
GT -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
              Ordering
EQ -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
p1
              Ordering
LT -> (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top) (ZDD a -> ST s (ZDD a)
f ZDD a
p0) (ZDD a -> ST s (ZDD a)
f ZDD a
p1)
            HashTable s (ZDD a) (ZDD a) -> ZDD a -> ZDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a) (ZDD a)
h ZDD a
p ZDD a
ret
            ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
  ZDD a -> ST s (ZDD a)
f ZDD a
zdd

-- | Subsets that does not contain a particular element
subset0 :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a
subset0 :: Int -> ZDD a -> ZDD a
subset0 Int
var ZDD a
zdd = (forall s. ST s (ZDD a)) -> ZDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (ZDD a)) -> ZDD a)
-> (forall s. ST s (ZDD a)) -> ZDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (ZDD a) (ZDD a)
h <- Int -> ST s (HashTable s (ZDD a) (ZDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: ZDD a -> ST s (ZDD a)
f p :: ZDD a
p@ZDD a
Base = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
p
      f ZDD a
Empty = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f p :: ZDD a
p@(Branch Int
top ZDD a
p0 ZDD a
p1) = do
        Maybe (ZDD a)
m <- HashTable s (ZDD a) (ZDD a) -> ZDD a -> ST s (Maybe (ZDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a) (ZDD a)
h ZDD a
p
        case Maybe (ZDD a)
m of
          Just ZDD a
ret -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
          Maybe (ZDD a)
Nothing -> do
            ZDD a
ret <- case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
top Int
var of
              Ordering
GT -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
p
              Ordering
EQ -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
p0
              Ordering
LT -> (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top) (ZDD a -> ST s (ZDD a)
f ZDD a
p0) (ZDD a -> ST s (ZDD a)
f ZDD a
p1)
            HashTable s (ZDD a) (ZDD a) -> ZDD a -> ZDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a) (ZDD a)
h ZDD a
p ZDD a
ret
            ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
  ZDD a -> ST s (ZDD a)
f ZDD a
zdd

-- | Insert a set into the ZDD.
insert :: forall a. ItemOrder a => IntSet -> ZDD a -> ZDD a
insert :: IntSet -> ZDD a -> ZDD a
insert IntSet
xs = [Int] -> ZDD a -> ZDD a
f ((Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) (IntSet -> [Int]
IntSet.toList IntSet
xs))
  where
    f :: [Int] -> ZDD a -> ZDD a
f [] ZDD a
Empty = ZDD a
forall a. ZDD a
Base
    f [] ZDD a
Base = ZDD a
forall a. ZDD a
Base
    f [] (Branch Int
top ZDD a
p0 ZDD a
p1) = Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top ([Int] -> ZDD a -> ZDD a
f [] ZDD a
p0) ZDD a
p1
    f (Int
y : [Int]
ys) ZDD a
Empty = Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
y ZDD a
forall a. ZDD a
Empty ([Int] -> ZDD a -> ZDD a
f [Int]
ys ZDD a
forall a. ZDD a
Empty)
    f (Int
y : [Int]
ys) ZDD a
Base = Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
y ZDD a
forall a. ZDD a
Base ([Int] -> ZDD a -> ZDD a
f [Int]
ys ZDD a
forall a. ZDD a
Empty)
    f yys :: [Int]
yys@(Int
y : [Int]
ys) p :: ZDD a
p@(Branch Int
top ZDD a
p0 ZDD a
p1) =
      case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
y Int
top of
        Ordering
LT -> Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
y ZDD a
p ([Int] -> ZDD a -> ZDD a
f [Int]
ys ZDD a
forall a. ZDD a
Empty)
        Ordering
GT -> Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top ([Int] -> ZDD a -> ZDD a
f [Int]
yys ZDD a
p0) ZDD a
p1
        Ordering
EQ -> Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top ZDD a
p0 ([Int] -> ZDD a -> ZDD a
f [Int]
ys ZDD a
p1)

-- | Delete a set from the ZDD.
delete :: forall a. ItemOrder a => IntSet -> ZDD a -> ZDD a
delete :: IntSet -> ZDD a -> ZDD a
delete IntSet
xs = [Int] -> ZDD a -> ZDD a
f ((Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) (IntSet -> [Int]
IntSet.toList IntSet
xs))
  where
    f :: [Int] -> ZDD a -> ZDD a
f [] ZDD a
Empty = ZDD a
forall a. ZDD a
Empty
    f [] ZDD a
Base = ZDD a
forall a. ZDD a
Empty
    f [] (Branch Int
top ZDD a
p0 ZDD a
p1) = Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top ([Int] -> ZDD a -> ZDD a
f [] ZDD a
p0) ZDD a
p1
    f (Int
_ : [Int]
_) ZDD a
Empty = ZDD a
forall a. ZDD a
Empty
    f (Int
_ : [Int]
_) ZDD a
Base = ZDD a
forall a. ZDD a
Base
    f yys :: [Int]
yys@(Int
y : [Int]
ys) p :: ZDD a
p@(Branch Int
top ZDD a
p0 ZDD a
p1) =
      case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
y Int
top of
        Ordering
LT -> ZDD a
p
        Ordering
GT -> Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top ([Int] -> ZDD a -> ZDD a
f [Int]
yys ZDD a
p0) ZDD a
p1
        Ordering
EQ -> Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top ZDD a
p0 ([Int] -> ZDD a -> ZDD a
f [Int]
ys ZDD a
p1)

-- | Insert an item into each element set of ZDD.
mapInsert :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a
mapInsert :: Int -> ZDD a -> ZDD a
mapInsert Int
var ZDD a
zdd = (forall s. ST s (ZDD a)) -> ZDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (ZDD a)) -> ZDD a)
-> (forall s. ST s (ZDD a)) -> ZDD a
forall a b. (a -> b) -> a -> b
$ do
  ZDD a -> ZDD a -> ST s (ZDD a)
unionOp <- ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkUnionOp
  HashTable s (ZDD a) (ZDD a)
h <- Int -> ST s (HashTable s (ZDD a) (ZDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: ZDD a -> ST s (ZDD a)
f p :: ZDD a
p@ZDD a
Base = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
var ZDD a
forall a. ZDD a
Empty ZDD a
p)
      f ZDD a
Empty = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f p :: ZDD a
p@(Branch Int
top ZDD a
p0 ZDD a
p1) = do
        Maybe (ZDD a)
m <- HashTable s (ZDD a) (ZDD a) -> ZDD a -> ST s (Maybe (ZDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a) (ZDD a)
h ZDD a
p
        case Maybe (ZDD a)
m of
          Just ZDD a
ret -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
          Maybe (ZDD a)
Nothing -> do
            ZDD a
ret <- case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
top Int
var of
              Ordering
GT -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
var ZDD a
forall a. ZDD a
Empty ZDD a
p)
              Ordering
LT -> (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top) (ZDD a -> ST s (ZDD a)
f ZDD a
p0) (ZDD a -> ST s (ZDD a)
f ZDD a
p1)
              Ordering
EQ -> (ZDD a -> ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top ZDD a
forall a. ZDD a
Empty) (ZDD a -> ZDD a -> ST s (ZDD a)
unionOp ZDD a
p0 ZDD a
p1)
            HashTable s (ZDD a) (ZDD a) -> ZDD a -> ZDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a) (ZDD a)
h ZDD a
p ZDD a
ret
            ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
  ZDD a -> ST s (ZDD a)
f ZDD a
zdd

-- | Delete an item from each element set of ZDD.
mapDelete :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a
mapDelete :: Int -> ZDD a -> ZDD a
mapDelete Int
var ZDD a
zdd = (forall s. ST s (ZDD a)) -> ZDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (ZDD a)) -> ZDD a)
-> (forall s. ST s (ZDD a)) -> ZDD a
forall a b. (a -> b) -> a -> b
$ do
  ZDD a -> ZDD a -> ST s (ZDD a)
unionOp <- ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkUnionOp
  HashTable s (ZDD a) (ZDD a)
h <- Int -> ST s (HashTable s (ZDD a) (ZDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: ZDD a -> ST s (ZDD a)
f ZDD a
Base = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Base
      f ZDD a
Empty = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f p :: ZDD a
p@(Branch Int
top ZDD a
p0 ZDD a
p1) = do
        Maybe (ZDD a)
m <- HashTable s (ZDD a) (ZDD a) -> ZDD a -> ST s (Maybe (ZDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a) (ZDD a)
h ZDD a
p
        case Maybe (ZDD a)
m of
          Just ZDD a
ret -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
          Maybe (ZDD a)
Nothing -> do
            ZDD a
ret <- case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
top Int
var of
              Ordering
GT -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
p
              Ordering
LT -> (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top) (ZDD a -> ST s (ZDD a)
f ZDD a
p0) (ZDD a -> ST s (ZDD a)
f ZDD a
p1)
              Ordering
EQ -> ZDD a -> ZDD a -> ST s (ZDD a)
unionOp ZDD a
p0 ZDD a
p1
            HashTable s (ZDD a) (ZDD a) -> ZDD a -> ZDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a) (ZDD a)
h ZDD a
p ZDD a
ret
            ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
  ZDD a -> ST s (ZDD a)
f ZDD a
zdd

-- | @change x p@ returns {if x∈s then s∖{x} else s∪{x} | s∈P}
change :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a
change :: Int -> ZDD a -> ZDD a
change Int
var ZDD a
zdd = (forall s. ST s (ZDD a)) -> ZDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (ZDD a)) -> ZDD a)
-> (forall s. ST s (ZDD a)) -> ZDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (ZDD a) (ZDD a)
h <- Int -> ST s (HashTable s (ZDD a) (ZDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: ZDD a -> ST s (ZDD a)
f p :: ZDD a
p@ZDD a
Base = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
var ZDD a
forall a. ZDD a
Empty ZDD a
p)
      f ZDD a
Empty = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f p :: ZDD a
p@(Branch Int
top ZDD a
p0 ZDD a
p1) = do
        Maybe (ZDD a)
m <- HashTable s (ZDD a) (ZDD a) -> ZDD a -> ST s (Maybe (ZDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a) (ZDD a)
h ZDD a
p
        case Maybe (ZDD a)
m of
          Just ZDD a
ret -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
          Maybe (ZDD a)
Nothing -> do
            ZDD a
ret <- case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
top Int
var of
              Ordering
GT -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
var ZDD a
forall a. ZDD a
Empty ZDD a
p)
              Ordering
EQ -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
var ZDD a
p1 ZDD a
p0)
              Ordering
LT -> (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top) (ZDD a -> ST s (ZDD a)
f ZDD a
p0) (ZDD a -> ST s (ZDD a)
f ZDD a
p1)
            HashTable s (ZDD a) (ZDD a) -> ZDD a -> ZDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a) (ZDD a)
h ZDD a
p ZDD a
ret
            ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
  ZDD a -> ST s (ZDD a)
f ZDD a
zdd

-- | Union of two family of sets.
union :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a
union :: ZDD a -> ZDD a -> ZDD a
union ZDD a
zdd1 ZDD a
zdd2 = (forall s. ST s (ZDD a)) -> ZDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (ZDD a)) -> ZDD a)
-> (forall s. ST s (ZDD a)) -> ZDD a
forall a b. (a -> b) -> a -> b
$ do
  ZDD a -> ZDD a -> ST s (ZDD a)
op <- ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkUnionOp
  ZDD a -> ZDD a -> ST s (ZDD a)
op ZDD a
zdd1 ZDD a
zdd2

mkUnionOp :: forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkUnionOp :: ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkUnionOp = do
  HashTable s (ZDD a, ZDD a) (ZDD a)
h <- Int -> ST s (HashTable s (ZDD a, ZDD a) (ZDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
Empty ZDD a
q = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
q
      f ZDD a
p ZDD a
Empty = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
p
      f ZDD a
p ZDD a
q | ZDD a
p ZDD a -> ZDD a -> Bool
forall a. Eq a => a -> a -> Bool
== ZDD a
q = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
p
      f ZDD a
p ZDD a
q = do
        let key :: (ZDD a, ZDD a)
key = if ZDD a -> Int
forall a. ZDD a -> Int
nodeId ZDD a
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= ZDD a -> Int
forall a. ZDD a -> Int
nodeId ZDD a
q then (ZDD a
p, ZDD a
q) else (ZDD a
q, ZDD a
p)
        Maybe (ZDD a)
m <- HashTable s (ZDD a, ZDD a) (ZDD a)
-> (ZDD a, ZDD a) -> ST s (Maybe (ZDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a, ZDD a) (ZDD a)
h (ZDD a, ZDD a)
key
        case Maybe (ZDD a)
m of
          Just ZDD a
ret -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
          Maybe (ZDD a)
Nothing -> do
            ZDD a
ret <- case Proxy a -> ZDD a -> ZDD a -> ZDDCase2 a
forall a. ItemOrder a => Proxy a -> ZDD a -> ZDD a -> ZDDCase2 a
zddCase2 (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) ZDD a
p ZDD a
q of
              ZDDCase2LT Int
ptop ZDD a
p0 ZDD a
p1 -> (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
ptop) (ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p0 ZDD a
q) (ZDD a -> ST s (ZDD a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ZDD a
p1)
              ZDDCase2GT Int
qtop ZDD a
q0 ZDD a
q1 -> (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
qtop) (ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p ZDD a
q0) (ZDD a -> ST s (ZDD a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ZDD a
q1)
              ZDDCase2EQ Int
top ZDD a
p0 ZDD a
p1 ZDD a
q0 ZDD a
q1 -> (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top) (ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p0 ZDD a
q0) (ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p1 ZDD a
q1)
              ZDDCase2EQ2 Bool
_ Bool
_ -> String -> ST s (ZDD a)
forall a. HasCallStack => String -> a
error String
"union: should not happen"
            HashTable s (ZDD a, ZDD a) (ZDD a)
-> (ZDD a, ZDD a) -> ZDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a, ZDD a) (ZDD a)
h (ZDD a, ZDD a)
key ZDD a
ret
            ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
  (ZDD a -> ZDD a -> ST s (ZDD a))
-> ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a -> ZDD a -> ST s (ZDD a)
f

-- | Unions of a list of ZDDs.
unions :: forall f a. (Foldable f, ItemOrder a) => f (ZDD a) -> ZDD a
unions :: f (ZDD a) -> ZDD a
unions f (ZDD a)
xs = (forall s. ST s (ZDD a)) -> ZDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (ZDD a)) -> ZDD a)
-> (forall s. ST s (ZDD a)) -> ZDD a
forall a b. (a -> b) -> a -> b
$ do
  ZDD a -> ZDD a -> ST s (ZDD a)
op <- ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkUnionOp
  (ZDD a -> ZDD a -> ST s (ZDD a))
-> ZDD a -> f (ZDD a) -> ST s (ZDD a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ZDD a -> ZDD a -> ST s (ZDD a)
op ZDD a
forall a. ZDD a
empty f (ZDD a)
xs

-- | Intersection of two family of sets.
intersection :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a
intersection :: ZDD a -> ZDD a -> ZDD a
intersection ZDD a
zdd1 ZDD a
zdd2 = (forall s. ST s (ZDD a)) -> ZDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (ZDD a)) -> ZDD a)
-> (forall s. ST s (ZDD a)) -> ZDD a
forall a b. (a -> b) -> a -> b
$ do
  ZDD a -> ZDD a -> ST s (ZDD a)
op <- ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkIntersectionOp
  ZDD a -> ZDD a -> ST s (ZDD a)
op ZDD a
zdd1 ZDD a
zdd2

mkIntersectionOp :: forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkIntersectionOp :: ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkIntersectionOp = do
  HashTable s (ZDD a, ZDD a) (ZDD a)
h <- Int -> ST s (HashTable s (ZDD a, ZDD a) (ZDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
Empty ZDD a
_q = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f ZDD a
_p ZDD a
Empty = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f ZDD a
p ZDD a
q | ZDD a
p ZDD a -> ZDD a -> Bool
forall a. Eq a => a -> a -> Bool
== ZDD a
q = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
p
      f ZDD a
p ZDD a
q = do
        let key :: (ZDD a, ZDD a)
key = if ZDD a -> Int
forall a. ZDD a -> Int
nodeId ZDD a
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= ZDD a -> Int
forall a. ZDD a -> Int
nodeId ZDD a
q then (ZDD a
p, ZDD a
q) else (ZDD a
q, ZDD a
p)
        Maybe (ZDD a)
m <- HashTable s (ZDD a, ZDD a) (ZDD a)
-> (ZDD a, ZDD a) -> ST s (Maybe (ZDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a, ZDD a) (ZDD a)
h (ZDD a, ZDD a)
key
        case Maybe (ZDD a)
m of
          Just ZDD a
ret -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
          Maybe (ZDD a)
Nothing -> do
            ZDD a
ret <- case Proxy a -> ZDD a -> ZDD a -> ZDDCase2 a
forall a. ItemOrder a => Proxy a -> ZDD a -> ZDD a -> ZDDCase2 a
zddCase2 (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) ZDD a
p ZDD a
q of
              ZDDCase2LT Int
_ptop ZDD a
p0 ZDD a
_p1 -> ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p0 ZDD a
q
              ZDDCase2GT Int
_qtop ZDD a
q0 ZDD a
_q1 -> ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p ZDD a
q0
              ZDDCase2EQ Int
top ZDD a
p0 ZDD a
p1 ZDD a
q0 ZDD a
q1 -> (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top) (ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p0 ZDD a
q0) (ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p1 ZDD a
q1)
              ZDDCase2EQ2 Bool
_ Bool
_ -> String -> ST s (ZDD a)
forall a. HasCallStack => String -> a
error String
"intersection: should not happen"
            HashTable s (ZDD a, ZDD a) (ZDD a)
-> (ZDD a, ZDD a) -> ZDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a, ZDD a) (ZDD a)
h (ZDD a, ZDD a)
key ZDD a
ret
            ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
  (ZDD a -> ZDD a -> ST s (ZDD a))
-> ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a -> ZDD a -> ST s (ZDD a)
f

-- | Difference of two family of sets.
difference :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a
difference :: ZDD a -> ZDD a -> ZDD a
difference ZDD a
zdd1 ZDD a
zdd2 = (forall s. ST s (ZDD a)) -> ZDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (ZDD a)) -> ZDD a)
-> (forall s. ST s (ZDD a)) -> ZDD a
forall a b. (a -> b) -> a -> b
$ do
  ZDD a -> ZDD a -> ST s (ZDD a)
op <- ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkDifferenceOp
  ZDD a -> ZDD a -> ST s (ZDD a)
op ZDD a
zdd1 ZDD a
zdd2

mkDifferenceOp :: forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkDifferenceOp :: ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkDifferenceOp = do
  HashTable s (ZDD a, ZDD a) (ZDD a)
h <- Int -> ST s (HashTable s (ZDD a, ZDD a) (ZDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
Empty ZDD a
_ = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f ZDD a
p ZDD a
Empty = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
p
      f ZDD a
p ZDD a
q | ZDD a
p ZDD a -> ZDD a -> Bool
forall a. Eq a => a -> a -> Bool
== ZDD a
q = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f ZDD a
p ZDD a
q = do
        Maybe (ZDD a)
m <- HashTable s (ZDD a, ZDD a) (ZDD a)
-> (ZDD a, ZDD a) -> ST s (Maybe (ZDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a, ZDD a) (ZDD a)
h (ZDD a
p, ZDD a
q)
        case Maybe (ZDD a)
m of
          Just ZDD a
ret -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
          Maybe (ZDD a)
Nothing -> do
            ZDD a
ret <- case Proxy a -> ZDD a -> ZDD a -> ZDDCase2 a
forall a. ItemOrder a => Proxy a -> ZDD a -> ZDD a -> ZDDCase2 a
zddCase2 (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) ZDD a
p ZDD a
q of
              ZDDCase2LT Int
ptop ZDD a
p0 ZDD a
p1 -> (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
ptop) (ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p0 ZDD a
q) (ZDD a -> ST s (ZDD a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ZDD a
p1)
              ZDDCase2GT Int
_qtop ZDD a
q0 ZDD a
_q1 -> ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p ZDD a
q0
              ZDDCase2EQ Int
top ZDD a
p0 ZDD a
p1 ZDD a
q0 ZDD a
q1 -> (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top) (ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p0 ZDD a
q0) (ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p1 ZDD a
q1)
              ZDDCase2EQ2 Bool
_ Bool
_ -> String -> ST s (ZDD a)
forall a. HasCallStack => String -> a
error String
"difference: should not happen"
            HashTable s (ZDD a, ZDD a) (ZDD a)
-> (ZDD a, ZDD a) -> ZDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a, ZDD a) (ZDD a)
h (ZDD a
p, ZDD a
q) ZDD a
ret
            ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
  (ZDD a -> ZDD a -> ST s (ZDD a))
-> ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a -> ZDD a -> ST s (ZDD a)
f

-- | See 'difference'
(\\) :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a
ZDD a
m1 \\ :: ZDD a -> ZDD a -> ZDD a
\\ ZDD a
m2 = ZDD a -> ZDD a -> ZDD a
forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a
difference ZDD a
m1 ZDD a
m2

-- | Given a family P and Q, it computes {S∈P | ∀X∈Q. X⊈S}
--
-- Sometimes it is denoted as /P ↘ Q/.
nonSuperset :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a
nonSuperset :: ZDD a -> ZDD a -> ZDD a
nonSuperset ZDD a
zdd1 ZDD a
zdd2 = (forall s. ST s (ZDD a)) -> ZDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (ZDD a)) -> ZDD a)
-> (forall s. ST s (ZDD a)) -> ZDD a
forall a b. (a -> b) -> a -> b
$ do
  ZDD a -> ZDD a -> ST s (ZDD a)
op <- ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkNonSueprsetOp
  ZDD a -> ZDD a -> ST s (ZDD a)
op ZDD a
zdd1 ZDD a
zdd2

mkNonSueprsetOp :: forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkNonSueprsetOp :: ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkNonSueprsetOp = do
  ZDD a -> ZDD a -> ST s (ZDD a)
intersectionOp <- ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkIntersectionOp 
  HashTable s (ZDD a, ZDD a) (ZDD a)
h <- Int -> ST s (HashTable s (ZDD a, ZDD a) (ZDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
Empty ZDD a
_ = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f ZDD a
_ ZDD a
Base = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f ZDD a
p ZDD a
Empty = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
p
      f ZDD a
p ZDD a
q | ZDD a
p ZDD a -> ZDD a -> Bool
forall a. Eq a => a -> a -> Bool
== ZDD a
q = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f ZDD a
p ZDD a
q = do
        Maybe (ZDD a)
m <- HashTable s (ZDD a, ZDD a) (ZDD a)
-> (ZDD a, ZDD a) -> ST s (Maybe (ZDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a, ZDD a) (ZDD a)
h (ZDD a
p, ZDD a
q)
        case Maybe (ZDD a)
m of
          Just ZDD a
ret -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
          Maybe (ZDD a)
Nothing -> do
            ZDD a
ret <- case Proxy a -> ZDD a -> ZDD a -> ZDDCase2 a
forall a. ItemOrder a => Proxy a -> ZDD a -> ZDD a -> ZDDCase2 a
zddCase2 (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) ZDD a
p ZDD a
q of
              ZDDCase2LT Int
ptop ZDD a
p0 ZDD a
p1 -> (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
ptop) (ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p0 ZDD a
q) (ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p1 ZDD a
q)
              ZDDCase2GT Int
_qtop ZDD a
q0 ZDD a
_q1 -> ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p ZDD a
q0
              ZDDCase2EQ Int
top ZDD a
p0 ZDD a
p1 ZDD a
q0 ZDD a
q1 -> do
                ZDD a
r0 <- ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p1 ZDD a
q0
                ZDD a
r1 <- ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p1 ZDD a
q1
                (ZDD a -> ZDD a -> ZDD a)
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top) (ZDD a -> ZDD a -> ST s (ZDD a)
f ZDD a
p0 ZDD a
q0) (ZDD a -> ZDD a -> ST s (ZDD a)
intersectionOp ZDD a
r0 ZDD a
r1)
              ZDDCase2EQ2 Bool
_ Bool
_ -> String -> ST s (ZDD a)
forall a. HasCallStack => String -> a
error String
"nonSuperset: should not happen"
            HashTable s (ZDD a, ZDD a) (ZDD a)
-> (ZDD a, ZDD a) -> ZDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a, ZDD a) (ZDD a)
h (ZDD a
p, ZDD a
q) ZDD a
ret
            ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
  (ZDD a -> ZDD a -> ST s (ZDD a))
-> ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a -> ZDD a -> ST s (ZDD a)
f

minimalHittingSetsKnuth' :: forall a. ItemOrder a => Bool -> ZDD a -> ZDD a
minimalHittingSetsKnuth' :: Bool -> ZDD a -> ZDD a
minimalHittingSetsKnuth' Bool
imai ZDD a
zdd = (forall s. ST s (ZDD a)) -> ZDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (ZDD a)) -> ZDD a)
-> (forall s. ST s (ZDD a)) -> ZDD a
forall a b. (a -> b) -> a -> b
$ do
  ZDD a -> ZDD a -> ST s (ZDD a)
unionOp <- ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkUnionOp
  ZDD a -> ZDD a -> ST s (ZDD a)
diffOp <- if Bool
imai then ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkDifferenceOp else ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkNonSueprsetOp
  HashTable s (ZDD a) (ZDD a)
h <- Int -> ST s (HashTable s (ZDD a) (ZDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: ZDD a -> ST s (ZDD a)
f ZDD a
Empty = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Base
      f ZDD a
Base = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f p :: ZDD a
p@(Branch Int
top ZDD a
p0 ZDD a
p1) = do
        Maybe (ZDD a)
m <- HashTable s (ZDD a) (ZDD a) -> ZDD a -> ST s (Maybe (ZDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a) (ZDD a)
h ZDD a
p
        case Maybe (ZDD a)
m of
          Just ZDD a
ret -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
          Maybe (ZDD a)
Nothing -> do
            ZDD a
r0 <- ZDD a -> ST s (ZDD a)
f (ZDD a -> ST s (ZDD a)) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ZDD a -> ZDD a -> ST s (ZDD a)
unionOp ZDD a
p0 ZDD a
p1
            ZDD a
r1 <- ST s (ST s (ZDD a)) -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ST s (ST s (ZDD a)) -> ST s (ZDD a))
-> ST s (ST s (ZDD a)) -> ST s (ZDD a)
forall a b. (a -> b) -> a -> b
$ (ZDD a -> ZDD a -> ST s (ZDD a))
-> ST s (ZDD a) -> ST s (ZDD a) -> ST s (ST s (ZDD a))
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 ZDD a -> ZDD a -> ST s (ZDD a)
diffOp (ZDD a -> ST s (ZDD a)
f ZDD a
p0) (ZDD a -> ST s (ZDD a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ZDD a
r0)
            let ret :: ZDD a
ret = Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
top ZDD a
r0 ZDD a
r1
            HashTable s (ZDD a) (ZDD a) -> ZDD a -> ZDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a) (ZDD a)
h ZDD a
p ZDD a
ret
            ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
  ZDD a -> ST s (ZDD a)
f ZDD a
zdd

-- | Minimal hitting sets.
--
-- D. E. Knuth, "The Art of Computer Programming, Volume 4A:
-- Combinatorial Algorithms, Part 1," Addison-Wesley Professional,
-- 2011.
minimalHittingSetsKnuth :: forall a. ItemOrder a => ZDD a -> ZDD a
minimalHittingSetsKnuth :: ZDD a -> ZDD a
minimalHittingSetsKnuth = Bool -> ZDD a -> ZDD a
forall a. ItemOrder a => Bool -> ZDD a -> ZDD a
minimalHittingSetsKnuth' Bool
False

-- | Minimal hitting sets.
--
-- T. Imai, "One-line hack of knuth's algorithm for minimal hitting set
-- computation with ZDDs," vol. 2015-AL-155, no. 15, Nov. 2015, pp. 1-3.
-- [Online]. Available: <http://id.nii.ac.jp/1001/00145799/>.
minimalHittingSetsImai :: forall a. ItemOrder a => ZDD a -> ZDD a
minimalHittingSetsImai :: ZDD a -> ZDD a
minimalHittingSetsImai = Bool -> ZDD a -> ZDD a
forall a. ItemOrder a => Bool -> ZDD a -> ZDD a
minimalHittingSetsKnuth' Bool
True

-- | Minimal hitting sets.
--
-- * T. Toda, “Hypergraph Transversal Computation with Binary Decision Diagrams,”
--   SEA 2013: Experimental Algorithms.
--   Available: <http://dx.doi.org/10.1007/978-3-642-38527-8_10>.
--
-- * HTC-BDD: Hypergraph Transversal Computation with Binary Decision Diagrams
--   <https://www.disc.lab.uec.ac.jp/toda/htcbdd.html>
minimalHittingSetsToda :: forall a. ItemOrder a => ZDD a -> ZDD a
minimalHittingSetsToda :: ZDD a -> ZDD a
minimalHittingSetsToda = BDD a -> ZDD a
forall a. ItemOrder a => BDD a -> ZDD a
minimal (BDD a -> ZDD a) -> (ZDD a -> BDD a) -> ZDD a -> ZDD a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ZDD a -> BDD a
forall a. ItemOrder a => ZDD a -> BDD a
hittingSetsBDD

hittingSetsBDD :: forall a. ItemOrder a => ZDD a -> BDD.BDD a
hittingSetsBDD :: ZDD a -> BDD a
hittingSetsBDD = BDD a
-> BDD a -> (Int -> BDD a -> BDD a -> BDD a) -> ZDD a -> BDD a
forall b a. b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
fold' BDD a
forall a. BDD a
BDD.true BDD a
forall a. BDD a
BDD.false (\Int
top BDD a
h0 BDD a
h1 -> BDD a
h0 BDD a -> BDD a -> BDD a
forall a. ItemOrder a => BDD a -> BDD a -> BDD a
BDD..&&. Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
BDD.Branch Int
top BDD a
h1 BDD a
forall a. BDD a
BDD.true)

minimal :: forall a. ItemOrder a => BDD.BDD a -> ZDD a
minimal :: BDD a -> ZDD a
minimal BDD a
bdd = (forall s. ST s (ZDD a)) -> ZDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (ZDD a)) -> ZDD a)
-> (forall s. ST s (ZDD a)) -> ZDD a
forall a b. (a -> b) -> a -> b
$ do
  ZDD a -> ZDD a -> ST s (ZDD a)
diffOp <- ST s (ZDD a -> ZDD a -> ST s (ZDD a))
forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))
mkDifferenceOp
  HashTable s (BDD a) (ZDD a)
h <- Int -> ST s (HashTable s (BDD a) (ZDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s (ZDD a)
f BDD a
BDD.F = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Empty
      f BDD a
BDD.T = ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
forall a. ZDD a
Base
      f p :: BDD a
p@(BDD.Branch Int
x BDD a
lo BDD a
hi) = do
        Maybe (ZDD a)
m <- HashTable s (BDD a) (ZDD a) -> BDD a -> ST s (Maybe (ZDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a) (ZDD a)
h BDD a
p
        case Maybe (ZDD a)
m of
          Just ZDD a
ret -> ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
          Maybe (ZDD a)
Nothing -> do
            ZDD a
ml <- BDD a -> ST s (ZDD a)
f BDD a
lo
            ZDD a
mh <- BDD a -> ST s (ZDD a)
f BDD a
hi
            ZDD a
ret <- (ZDD a -> ZDD a) -> ST s (ZDD a) -> ST s (ZDD a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
x ZDD a
ml) (ZDD a -> ZDD a -> ST s (ZDD a)
diffOp ZDD a
mh ZDD a
ml)
            HashTable s (BDD a) (ZDD a) -> BDD a -> ZDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a) (ZDD a)
h BDD a
p ZDD a
ret
            ZDD a -> ST s (ZDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ZDD a
ret
  BDD a -> ST s (ZDD a)
f BDD a
bdd

-- | See 'minimalHittingSetsToda'.
minimalHittingSets :: forall a. ItemOrder a => ZDD a -> ZDD a
minimalHittingSets :: ZDD a -> ZDD a
minimalHittingSets = ZDD a -> ZDD a
forall a. ItemOrder a => ZDD a -> ZDD a
minimalHittingSetsToda

-- | Is the set a member of the family?
member :: forall a. (ItemOrder a) => IntSet -> ZDD a -> Bool
member :: IntSet -> ZDD a -> Bool
member IntSet
xs = [Int] -> ZDD a -> Bool
forall a. ItemOrder a => [Int] -> ZDD a -> Bool
member' [Int]
xs'
  where
    xs' :: [Int]
xs' = (Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IntSet.toList IntSet
xs

member' :: forall a. (ItemOrder a) => [Int] -> ZDD a -> Bool
member' :: [Int] -> ZDD a -> Bool
member' [] ZDD a
Base = Bool
True
member' [] (Branch Int
_ ZDD a
p0 ZDD a
_) = [Int] -> ZDD a -> Bool
forall a. ItemOrder a => [Int] -> ZDD a -> Bool
member' [] ZDD a
p0
member' yys :: [Int]
yys@(Int
y:[Int]
ys) (Branch Int
top ZDD a
p0 ZDD a
p1) =
  case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
y Int
top of
    Ordering
EQ -> [Int] -> ZDD a -> Bool
forall a. ItemOrder a => [Int] -> ZDD a -> Bool
member' [Int]
ys ZDD a
p1
    Ordering
GT -> [Int] -> ZDD a -> Bool
forall a. ItemOrder a => [Int] -> ZDD a -> Bool
member' [Int]
yys ZDD a
p0
    Ordering
LT -> Bool
False
member' [Int]
_ ZDD a
_ = Bool
False

-- | Is the set not in the family?
notMember :: forall a. (ItemOrder a) => IntSet -> ZDD a -> Bool
notMember :: IntSet -> ZDD a -> Bool
notMember IntSet
xs = Bool -> Bool
not (Bool -> Bool) -> (ZDD a -> Bool) -> ZDD a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> ZDD a -> Bool
forall a. ItemOrder a => IntSet -> ZDD a -> Bool
member IntSet
xs

-- | Is this the empty set?
null :: ZDD a -> Bool
null :: ZDD a -> Bool
null = (ZDD a
forall a. ZDD a
empty ZDD a -> ZDD a -> Bool
forall a. Eq a => a -> a -> Bool
==)

{-# SPECIALIZE size :: ZDD a -> Int #-}
{-# SPECIALIZE size :: ZDD a -> Integer #-}
{-# SPECIALIZE size :: ZDD a -> Natural #-}
-- | The number of sets in the family.
size :: (Integral b) => ZDD a -> b
size :: ZDD a -> b
size = b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
forall b a. b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
fold' b
0 b
1 (\Int
_ b
n0 b
n1 -> b
n0 b -> b -> b
forall a. Num a => a -> a -> a
+ b
n1)

-- | @(s1 `isSubsetOf` s2)@ indicates whether @s1@ is a subset of @s2@.
isSubsetOf :: ItemOrder a => ZDD a -> ZDD a -> Bool
isSubsetOf :: ZDD a -> ZDD a -> Bool
isSubsetOf ZDD a
a ZDD a
b = ZDD a -> ZDD a -> ZDD a
forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a
union ZDD a
a ZDD a
b ZDD a -> ZDD a -> Bool
forall a. Eq a => a -> a -> Bool
== ZDD a
b

-- | @(s1 `isProperSubsetOf` s2)@ indicates whether @s1@ is a proper subset of @s2@.
isProperSubsetOf :: ItemOrder a => ZDD a -> ZDD a -> Bool
isProperSubsetOf :: ZDD a -> ZDD a -> Bool
isProperSubsetOf ZDD a
a ZDD a
b = ZDD a
a ZDD a -> ZDD a -> Bool
forall a. ItemOrder a => ZDD a -> ZDD a -> Bool
`isSubsetOf` ZDD a
b Bool -> Bool -> Bool
&& ZDD a
a ZDD a -> ZDD a -> Bool
forall a. Eq a => a -> a -> Bool
/= ZDD a
b

-- | Check whether two sets are disjoint (i.e., their intersection is empty).
disjoint :: ItemOrder a => ZDD a -> ZDD a -> Bool
disjoint :: ZDD a -> ZDD a -> Bool
disjoint ZDD a
a ZDD a
b = ZDD a -> Bool
forall a. ZDD a -> Bool
null (ZDD a
a ZDD a -> ZDD a -> ZDD a
forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a
`intersection` ZDD a
b)

--- | Unions of all member sets
flatten :: ItemOrder a => ZDD a -> IntSet
flatten :: ZDD a -> IntSet
flatten = IntSet
-> IntSet -> (Int -> IntSet -> IntSet -> IntSet) -> ZDD a -> IntSet
forall b a. b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
fold' IntSet
IntSet.empty IntSet
IntSet.empty (\Int
top IntSet
lo IntSet
hi -> Int -> IntSet -> IntSet
IntSet.insert Int
top (IntSet
lo IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
hi))

-- | Create a ZDD from a set of 'IntSet'
fromSetOfIntSets :: forall a. ItemOrder a => Set IntSet -> ZDD a
fromSetOfIntSets :: Set IntSet -> ZDD a
fromSetOfIntSets = [IntSet] -> ZDD a
forall a. ItemOrder a => [IntSet] -> ZDD a
fromListOfIntSets ([IntSet] -> ZDD a)
-> (Set IntSet -> [IntSet]) -> Set IntSet -> ZDD a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList

-- | Convert the family to a set of 'IntSet'.
toSetOfIntSets :: ZDD a -> Set IntSet
toSetOfIntSets :: ZDD a -> Set IntSet
toSetOfIntSets = Set IntSet
-> Set IntSet
-> (Int -> Set IntSet -> Set IntSet -> Set IntSet)
-> ZDD a
-> Set IntSet
forall b a. b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
fold' Set IntSet
forall a. Set a
Set.empty (IntSet -> Set IntSet
forall a. a -> Set a
Set.singleton IntSet
IntSet.empty) (\Int
top Set IntSet
lo Set IntSet
hi -> Set IntSet
lo Set IntSet -> Set IntSet -> Set IntSet
forall a. Semigroup a => a -> a -> a
<> (IntSet -> IntSet) -> Set IntSet -> Set IntSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.insert Int
top) Set IntSet
hi)

-- | Create a ZDD from a list of 'IntSet'
fromListOfIntSets :: forall a. ItemOrder a => [IntSet] -> ZDD a
fromListOfIntSets :: [IntSet] -> ZDD a
fromListOfIntSets = [[Int]] -> ZDD a
forall a. ItemOrder a => [[Int]] -> ZDD a
fromListOfSortedList ([[Int]] -> ZDD a) -> ([IntSet] -> [[Int]]) -> [IntSet] -> ZDD a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntSet -> [Int]) -> [IntSet] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map IntSet -> [Int]
f
  where
    f :: IntSet -> [Int]
    f :: IntSet -> [Int]
f = (Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) ([Int] -> [Int]) -> (IntSet -> [Int]) -> IntSet -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IntSet.toList

-- | Convert the family to a list of 'IntSet'.
toListOfIntSets :: ZDD a -> [IntSet]
toListOfIntSets :: ZDD a -> [IntSet]
toListOfIntSets = [IntSet]
-> [IntSet]
-> (Int -> [IntSet] -> [IntSet] -> [IntSet])
-> ZDD a
-> [IntSet]
forall b a. b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
fold [] [IntSet
IntSet.empty] (\Int
top [IntSet]
lo [IntSet]
hi -> [IntSet]
lo [IntSet] -> [IntSet] -> [IntSet]
forall a. Semigroup a => a -> a -> a
<> (IntSet -> IntSet) -> [IntSet] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> IntSet -> IntSet
IntSet.insert Int
top) [IntSet]
hi)

fromListOfSortedList :: forall a. ItemOrder a => [[Int]] -> ZDD a
fromListOfSortedList :: [[Int]] -> ZDD a
fromListOfSortedList = [ZDD a] -> ZDD a
forall (f :: * -> *) a.
(Foldable f, ItemOrder a) =>
f (ZDD a) -> ZDD a
unions ([ZDD a] -> ZDD a) -> ([[Int]] -> [ZDD a]) -> [[Int]] -> ZDD a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Int] -> ZDD a) -> [[Int]] -> [ZDD a]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> ZDD a
f
  where
    f :: [Int] -> ZDD a
    f :: [Int] -> ZDD a
f = (Int -> ZDD a -> ZDD a) -> ZDD a -> [Int] -> ZDD a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Int
x ZDD a
node -> Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
x ZDD a
forall a. ZDD a
Empty ZDD a
node) ZDD a
forall a. ZDD a
Base

-- | Fold over the graph structure of the ZDD.
--
-- It takes values for substituting 'empty' and 'base',
-- and a function for substiting non-terminal node.
fold :: b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
fold :: b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
fold b
ff b
tt Int -> b -> b -> b
br ZDD a
zdd = (forall s. ST s b) -> b
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s b) -> b) -> (forall s. ST s b) -> b
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (ZDD a) b
h <- Int -> ST s (HashTable s (ZDD a) b)
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: ZDD a -> ST s b
f ZDD a
Empty = b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
ff
      f ZDD a
Base = b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
tt
      f p :: ZDD a
p@(Branch Int
top ZDD a
p0 ZDD a
p1) = do
        Maybe b
m <- HashTable s (ZDD a) b -> ZDD a -> ST s (Maybe b)
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a) b
h ZDD a
p
        case Maybe b
m of
          Just b
ret -> b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
ret
          Maybe b
Nothing -> do
            b
r0 <- ZDD a -> ST s b
f ZDD a
p0
            b
r1 <- ZDD a -> ST s b
f ZDD a
p1
            let ret :: b
ret = Int -> b -> b -> b
br Int
top b
r0 b
r1
            HashTable s (ZDD a) b -> ZDD a -> b -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a) b
h ZDD a
p b
ret
            b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
ret
  ZDD a -> ST s b
f ZDD a
zdd

-- | Strict version of 'fold'
fold' :: b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
fold' :: b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
fold' !b
ff !b
tt Int -> b -> b -> b
br ZDD a
zdd = (forall s. ST s b) -> b
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s b) -> b) -> (forall s. ST s b) -> b
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (ZDD a) b
h <- Int -> ST s (HashTable s (ZDD a) b)
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: ZDD a -> ST s b
f ZDD a
Empty = b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
ff
      f ZDD a
Base = b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
tt
      f p :: ZDD a
p@(Branch Int
top ZDD a
p0 ZDD a
p1) = do
        Maybe b
m <- HashTable s (ZDD a) b -> ZDD a -> ST s (Maybe b)
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a) b
h ZDD a
p
        case Maybe b
m of
          Just b
ret -> b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
ret
          Maybe b
Nothing -> do
            b
r0 <- ZDD a -> ST s b
f ZDD a
p0
            b
r1 <- ZDD a -> ST s b
f ZDD a
p1
            let ret :: b
ret = Int -> b -> b -> b
br Int
top b
r0 b
r1
            b -> ST s () -> ST s ()
seq b
ret (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ HashTable s (ZDD a) b -> ZDD a -> b -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a) b
h ZDD a
p b
ret
            b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
ret
  ZDD a -> ST s b
f ZDD a
zdd

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

-- | Sample a set from uniform distribution over elements of the ZDD.
--
-- The function constructs a table internally and the table is shared across
-- multiple use of the resulting action (@m IntSet@).
-- Therefore, the code
--
-- @
-- let g = uniformM zdd gen
-- s1 <- g
-- s2 <- g
-- @
--
-- is more efficient than
--
-- @
-- s1 <- uniformM zdd gen
-- s2 <- uniformM zdd gen
-- @
-- .
#if MIN_VERSION_mwc_random(0,15,0)
uniformM :: forall a g m. (ItemOrder a, StatefulGen g m) => ZDD a -> g -> m IntSet
#else
uniformM :: forall a m. (ItemOrder a, PrimMonad m) => ZDD a -> Gen (PrimState m) -> m IntSet
#endif
uniformM :: ZDD a -> g -> m IntSet
uniformM ZDD a
Empty = String -> g -> m IntSet
forall a. HasCallStack => String -> a
error String
"Data.DecisionDiagram.ZDD.uniformM: empty ZDD"
uniformM ZDD a
zdd = g -> m IntSet
func
  where
    func :: g -> m IntSet
func g
gen = ZDD a -> [Int] -> m IntSet
f ZDD a
zdd []
      where
        f :: ZDD a -> [Int] -> m IntSet
f ZDD a
Empty [Int]
_ = String -> m IntSet
forall a. HasCallStack => String -> a
error String
"Data.DecisionDiagram.ZDD.uniformM: should not happen"
        f ZDD a
Base [Int]
r = IntSet -> m IntSet
forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet -> m IntSet) -> IntSet -> m IntSet
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList [Int]
r
        f p :: ZDD a
p@(Branch Int
top ZDD a
p0 ZDD a
p1) [Int]
r = do
          Bool
b <- Double -> g -> m Bool
forall g (m :: * -> *). StatefulGen g m => Double -> g -> m Bool
bernoulli (HashMap (ZDD a) Double
table HashMap (ZDD a) Double -> ZDD a -> Double
forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
HashMap.! ZDD a
p) g
gen
          if Bool
b then
            ZDD a -> [Int] -> m IntSet
f ZDD a
p1 (Int
top Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
r)
          else
            ZDD a -> [Int] -> m IntSet
f ZDD a
p0 [Int]
r

    table :: HashMap (ZDD a) Double
    table :: HashMap (ZDD a) Double
table = (forall s. ST s (HashMap (ZDD a) Double)) -> HashMap (ZDD a) Double
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (HashMap (ZDD a) Double))
 -> HashMap (ZDD a) Double)
-> (forall s. ST s (HashMap (ZDD a) Double))
-> HashMap (ZDD a) Double
forall a b. (a -> b) -> a -> b
$ do
      HashTable s (ZDD a) (Integer, Double)
h <- Int -> ST s (HashTable s (ZDD a) (Integer, Double))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
      let f :: ZDD a -> ST s Integer
f ZDD a
Empty = Integer -> ST s Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
0 :: Integer)
          f ZDD a
Base = Integer -> ST s Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
1
          f p :: ZDD a
p@(Branch Int
_ ZDD a
p0 ZDD a
p1) = do
            Maybe (Integer, Double)
m <- HashTable s (ZDD a) (Integer, Double)
-> ZDD a -> ST s (Maybe (Integer, Double))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a) (Integer, Double)
h ZDD a
p
            case Maybe (Integer, Double)
m of
              Just (Integer
ret, Double
_) -> Integer -> ST s Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
ret
              Maybe (Integer, Double)
Nothing -> do
                Integer
n0 <- ZDD a -> ST s Integer
f ZDD a
p0
                Integer
n1 <- ZDD a -> ST s Integer
f ZDD a
p1
                let s :: Integer
s = Integer
n0 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n1
                    r :: Double
                    r :: Double
r = Ratio Integer -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Integer
n1 Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% (Integer
n0 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n1))
                Double -> ST s () -> ST s ()
seq Double
r (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ HashTable s (ZDD a) (Integer, Double)
-> ZDD a -> (Integer, Double) -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a) (Integer, Double)
h ZDD a
p (Integer
s, Double
r)
                Integer -> ST s Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
s
      Integer
_ <- ZDD a -> ST s Integer
f ZDD a
zdd
      [(ZDD a, (Integer, Double))]
xs <- HashTable s (ZDD a) (Integer, Double)
-> ST s [(ZDD a, (Integer, Double))]
forall (h :: * -> * -> * -> *) s k v.
HashTable h =>
h s k v -> ST s [(k, v)]
H.toList HashTable s (ZDD a) (Integer, Double)
h
      HashMap (ZDD a) Double -> ST s (HashMap (ZDD a) Double)
forall (m :: * -> *) a. Monad m => a -> m a
return (HashMap (ZDD a) Double -> ST s (HashMap (ZDD a) Double))
-> HashMap (ZDD a) Double -> ST s (HashMap (ZDD a) Double)
forall a b. (a -> b) -> a -> b
$ [(ZDD a, Double)] -> HashMap (ZDD a) Double
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList [(ZDD a
n, Double
r) | (ZDD a
n, (Integer
_, Double
r)) <- [(ZDD a, (Integer, Double))]
xs]

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

-- | Find a minimum element set with respect to given weight function
--
-- \[
-- \min_{X\in S} \sum_{x\in X} w(x)
-- \]
findMinSum :: forall a w. (ItemOrder a, Num w, Ord w) => (Int -> w) -> ZDD a -> (w, IntSet)
findMinSum :: (Int -> w) -> ZDD a -> (w, IntSet)
findMinSum Int -> w
weight =
  (w, IntSet) -> Maybe (w, IntSet) -> (w, IntSet)
forall a. a -> Maybe a -> a
fromMaybe (String -> (w, IntSet)
forall a. HasCallStack => String -> a
error String
"Data.DecisionDiagram.ZDD.findMinSum: empty ZDD") (Maybe (w, IntSet) -> (w, IntSet))
-> (ZDD a -> Maybe (w, IntSet)) -> ZDD a -> (w, IntSet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Maybe (w, IntSet)
-> Maybe (w, IntSet)
-> (Int
    -> Maybe (w, IntSet) -> Maybe (w, IntSet) -> Maybe (w, IntSet))
-> ZDD a
-> Maybe (w, IntSet)
forall b a. b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
fold' Maybe (w, IntSet)
forall a. Maybe a
Nothing ((w, IntSet) -> Maybe (w, IntSet)
forall a. a -> Maybe a
Just (w
0, IntSet
IntSet.empty)) Int -> Maybe (w, IntSet) -> Maybe (w, IntSet) -> Maybe (w, IntSet)
f
  where
    f :: Int -> Maybe (w, IntSet) -> Maybe (w, IntSet) -> Maybe (w, IntSet)
f Int
_ Maybe (w, IntSet)
_ Maybe (w, IntSet)
Nothing = Maybe (w, IntSet)
forall a. HasCallStack => a
undefined
    f Int
x Maybe (w, IntSet)
z1 (Just (w
w2, IntSet
s2)) =
      case Maybe (w, IntSet)
z1 of
        Just (w
w1, IntSet
_) | w
w1 w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
w2' -> Maybe (w, IntSet)
z1
        Maybe (w, IntSet)
_ -> w -> Maybe (w, IntSet) -> Maybe (w, IntSet)
seq w
w2' (Maybe (w, IntSet) -> Maybe (w, IntSet))
-> Maybe (w, IntSet) -> Maybe (w, IntSet)
forall a b. (a -> b) -> a -> b
$ IntSet -> Maybe (w, IntSet) -> Maybe (w, IntSet)
seq IntSet
s2' (Maybe (w, IntSet) -> Maybe (w, IntSet))
-> Maybe (w, IntSet) -> Maybe (w, IntSet)
forall a b. (a -> b) -> a -> b
$ (w, IntSet) -> Maybe (w, IntSet)
forall a. a -> Maybe a
Just (w
w2', IntSet
s2')
      where
        w2' :: w
w2' = w
w2 w -> w -> w
forall a. Num a => a -> a -> a
+ Int -> w
weight Int
x
        s2' :: IntSet
s2' = Int -> IntSet -> IntSet
IntSet.insert Int
x IntSet
s2

-- | Find a maximum element set with respect to given weight function
--
-- \[
-- \max_{X\in S} \sum_{x\in X} w(x)
-- \]
findMaxSum :: forall a w. (ItemOrder a, Num w, Ord w) => (Int -> w) -> ZDD a -> (w, IntSet)
findMaxSum :: (Int -> w) -> ZDD a -> (w, IntSet)
findMaxSum Int -> w
weight =
  (w, IntSet) -> Maybe (w, IntSet) -> (w, IntSet)
forall a. a -> Maybe a -> a
fromMaybe (String -> (w, IntSet)
forall a. HasCallStack => String -> a
error String
"Data.DecisionDiagram.ZDD.findMinSum: empty ZDD") (Maybe (w, IntSet) -> (w, IntSet))
-> (ZDD a -> Maybe (w, IntSet)) -> ZDD a -> (w, IntSet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Maybe (w, IntSet)
-> Maybe (w, IntSet)
-> (Int
    -> Maybe (w, IntSet) -> Maybe (w, IntSet) -> Maybe (w, IntSet))
-> ZDD a
-> Maybe (w, IntSet)
forall b a. b -> b -> (Int -> b -> b -> b) -> ZDD a -> b
fold' Maybe (w, IntSet)
forall a. Maybe a
Nothing ((w, IntSet) -> Maybe (w, IntSet)
forall a. a -> Maybe a
Just (w
0, IntSet
IntSet.empty)) Int -> Maybe (w, IntSet) -> Maybe (w, IntSet) -> Maybe (w, IntSet)
f
  where
    f :: Int -> Maybe (w, IntSet) -> Maybe (w, IntSet) -> Maybe (w, IntSet)
f Int
_ Maybe (w, IntSet)
_ Maybe (w, IntSet)
Nothing = Maybe (w, IntSet)
forall a. HasCallStack => a
undefined
    f Int
x Maybe (w, IntSet)
z1 (Just (w
w2, IntSet
s2)) =
      case Maybe (w, IntSet)
z1 of
        Just (w
w1, IntSet
_) | w
w1 w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
w2' -> Maybe (w, IntSet)
z1
        Maybe (w, IntSet)
_ -> w -> Maybe (w, IntSet) -> Maybe (w, IntSet)
seq w
w2' (Maybe (w, IntSet) -> Maybe (w, IntSet))
-> Maybe (w, IntSet) -> Maybe (w, IntSet)
forall a b. (a -> b) -> a -> b
$ IntSet -> Maybe (w, IntSet) -> Maybe (w, IntSet)
seq IntSet
s2' (Maybe (w, IntSet) -> Maybe (w, IntSet))
-> Maybe (w, IntSet) -> Maybe (w, IntSet)
forall a b. (a -> b) -> a -> b
$ (w, IntSet) -> Maybe (w, IntSet)
forall a. a -> Maybe a
Just (w
w2', IntSet
s2')
      where
        w2' :: w
w2' = w
w2 w -> w -> w
forall a. Num a => a -> a -> a
+ Int -> w
weight Int
x
        s2' :: IntSet
s2' = Int -> IntSet -> IntSet
IntSet.insert Int
x IntSet
s2

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

type Graph = IntMap Node

data Node
  = NodeEmpty
  | NodeBase
  | NodeBranch !Int Int Int
  deriving (Node -> Node -> Bool
(Node -> Node -> Bool) -> (Node -> Node -> Bool) -> Eq Node
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Node -> Node -> Bool
$c/= :: Node -> Node -> Bool
== :: Node -> Node -> Bool
$c== :: Node -> Node -> Bool
Eq, Int -> Node -> ShowS
[Node] -> ShowS
Node -> String
(Int -> Node -> ShowS)
-> (Node -> String) -> ([Node] -> ShowS) -> Show Node
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Node] -> ShowS
$cshowList :: [Node] -> ShowS
show :: Node -> String
$cshow :: Node -> String
showsPrec :: Int -> Node -> ShowS
$cshowsPrec :: Int -> Node -> ShowS
Show, ReadPrec [Node]
ReadPrec Node
Int -> ReadS Node
ReadS [Node]
(Int -> ReadS Node)
-> ReadS [Node] -> ReadPrec Node -> ReadPrec [Node] -> Read Node
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Node]
$creadListPrec :: ReadPrec [Node]
readPrec :: ReadPrec Node
$creadPrec :: ReadPrec Node
readList :: ReadS [Node]
$creadList :: ReadS [Node]
readsPrec :: Int -> ReadS Node
$creadsPrec :: Int -> ReadS Node
Read)

-- | Convert a ZDD into a pointed graph
toGraph :: ZDD a -> (Graph, Int)
toGraph :: ZDD a -> (Graph, Int)
toGraph ZDD a
bdd =
  case Identity (ZDD a) -> (Graph, Identity Int)
forall (t :: * -> *) a.
Traversable t =>
t (ZDD a) -> (Graph, t Int)
toGraph' (ZDD a -> Identity (ZDD a)
forall a. a -> Identity a
Identity ZDD a
bdd) of
    (Graph
g, Identity Int
v) -> (Graph
g, Int
v)

-- | Convert multiple ZDDs into a graph
toGraph' :: Traversable t => t (ZDD a) -> (Graph, t Int)
toGraph' :: t (ZDD a) -> (Graph, t Int)
toGraph' t (ZDD a)
bs = (forall s. ST s (Graph, t Int)) -> (Graph, t Int)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Graph, t Int)) -> (Graph, t Int))
-> (forall s. ST s (Graph, t Int)) -> (Graph, t Int)
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (ZDD a) Int
h <- Int -> ST s (HashTable s (ZDD a) Int)
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  HashTable s (ZDD a) Int -> ZDD a -> Int -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a) Int
h ZDD a
forall a. ZDD a
Empty Int
0
  HashTable s (ZDD a) Int -> ZDD a -> Int -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a) Int
h ZDD a
forall a. ZDD a
Base Int
1
  STRef s Int
counter <- Int -> ST s (STRef s Int)
forall a s. a -> ST s (STRef s a)
newSTRef Int
2
  STRef s Graph
ref <- Graph -> ST s (STRef s Graph)
forall a s. a -> ST s (STRef s a)
newSTRef (Graph -> ST s (STRef s Graph)) -> Graph -> ST s (STRef s Graph)
forall a b. (a -> b) -> a -> b
$ [(Int, Node)] -> Graph
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int
0, Node
NodeEmpty), (Int
1, Node
NodeBase)]

  let f :: ZDD a -> ST s Int
f ZDD a
Empty = Int -> ST s Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
      f ZDD a
Base = Int -> ST s Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
      f p :: ZDD a
p@(Branch Int
x ZDD a
lo ZDD a
hi) = do
        Maybe Int
m <- HashTable s (ZDD a) Int -> ZDD a -> ST s (Maybe Int)
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (ZDD a) Int
h ZDD a
p
        case Maybe Int
m of
          Just Int
ret -> Int -> ST s Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
ret
          Maybe Int
Nothing -> do
            Int
r0 <- ZDD a -> ST s Int
f ZDD a
lo
            Int
r1 <- ZDD a -> ST s Int
f ZDD a
hi
            Int
n <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
counter
            STRef s Int -> Int -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Int
counter (Int -> ST s ()) -> Int -> ST s ()
forall a b. (a -> b) -> a -> b
$! Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1
            HashTable s (ZDD a) Int -> ZDD a -> Int -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (ZDD a) Int
h ZDD a
p Int
n
            STRef s Graph -> (Graph -> Graph) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef' STRef s Graph
ref (Int -> Node -> Graph -> Graph
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
n (Int -> Int -> Int -> Node
NodeBranch Int
x Int
r0 Int
r1))
            Int -> ST s Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n

  t Int
vs <- (ZDD a -> ST s Int) -> t (ZDD a) -> ST s (t Int)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ZDD a -> ST s Int
f t (ZDD a)
bs
  Graph
g <- STRef s Graph -> ST s Graph
forall s a. STRef s a -> ST s a
readSTRef STRef s Graph
ref
  (Graph, t Int) -> ST s (Graph, t Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Graph
g, t Int
vs)

-- | Convert a pointed graph into a ZDD
fromGraph :: (Graph, Int) -> ZDD a
fromGraph :: (Graph, Int) -> ZDD a
fromGraph (Graph
g, Int
v) =
  case Int -> IntMap (ZDD a) -> Maybe (ZDD a)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
v (Graph -> IntMap (ZDD a)
forall a. Graph -> IntMap (ZDD a)
fromGraph' Graph
g) of
    Maybe (ZDD a)
Nothing -> String -> ZDD a
forall a. HasCallStack => String -> a
error (String
"Data.DecisionDiagram.ZDD.fromGraph: invalid node id " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
v)
    Just ZDD a
bdd -> ZDD a
bdd

-- | Convert nodes of a graph into ZDDs
fromGraph' :: Graph -> IntMap (ZDD a)
fromGraph' :: Graph -> IntMap (ZDD a)
fromGraph' Graph
g = IntMap (ZDD a)
ret
  where
    ret :: IntMap (ZDD a)
ret = (Node -> ZDD a) -> Graph -> IntMap (ZDD a)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map Node -> ZDD a
f Graph
g
    f :: Node -> ZDD a
f Node
NodeEmpty = ZDD a
forall a. ZDD a
Empty
    f Node
NodeBase = ZDD a
forall a. ZDD a
Base
    f (NodeBranch Int
x Int
lo Int
hi) =
      case (Int -> IntMap (ZDD a) -> Maybe (ZDD a)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
lo IntMap (ZDD a)
ret, Int -> IntMap (ZDD a) -> Maybe (ZDD a)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
hi IntMap (ZDD a)
ret) of
        (Maybe (ZDD a)
Nothing, Maybe (ZDD a)
_) -> String -> ZDD a
forall a. HasCallStack => String -> a
error (String
"Data.DecisionDiagram.ZDD.fromGraph': invalid node id " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
lo)
        (Maybe (ZDD a)
_, Maybe (ZDD a)
Nothing) -> String -> ZDD a
forall a. HasCallStack => String -> a
error (String
"Data.DecisionDiagram.ZDD.fromGraph': invalid node id " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
hi)
        (Just ZDD a
lo', Just ZDD a
hi') -> Int -> ZDD a -> ZDD a -> ZDD a
forall a. Int -> ZDD a -> ZDD a -> ZDD a
Branch Int
x ZDD a
lo' ZDD a
hi'

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