{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
----------------------------------------------------------------------
-- |
-- Module      :  Data.DecisionDiagram.BDD
-- Copyright   :  (c) Masahiro Sakai 2021
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  unstable
-- Portability :  non-portable
--
-- Reduced Ordered Binary Decision Diagrams (ROBDD).
--
-- References:
--
-- * Bryant, "Graph-Based Algorithms for Boolean Function Manipulation,"
--   in IEEE Transactions on Computers, vol. C-35, no. 8, pp. 677-691,
--   Aug. 1986, doi: [10.1109/TC.1986.1676819](https://doi.org/10.1109/TC.1986.1676819).
--   <https://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf>
--
----------------------------------------------------------------------
module Data.DecisionDiagram.BDD
  (
  -- * The BDD type
    BDD (F, T, Branch)

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

  -- * Boolean operations
  , true
  , false
  , var
  , notB
  , (.&&.)
  , (.||.)
  , xor
  , (.=>.)
  , (.<=>.)
  , ite
  , andB
  , orB

  -- * Quantification
  , forAll
  , exists
  , existsUnique
  , forAllSet
  , existsSet
  , existsUniqueSet

  -- * Query
  , support
  , evaluate

  -- * Restriction / Cofactor
  , restrict
  , restrictSet
  , restrictLaw

  -- * Substition / Composition
  , subst
  , substSet

  -- * Fold
  , fold
  , fold'

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

import Control.Exception (assert)
import Control.Monad
import Control.Monad.ST
import Data.Function (on)
import Data.Functor.Identity
import Data.Hashable
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 (sortBy)
import Data.Proxy
import Data.STRef
import Text.Read

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

infixr 3 .&&.
infixr 2 .||.
infixr 1 .=>.
infix 1 .<=>.

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

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

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

-- | Reduced ordered binary decision diagram representing boolean function
newtype BDD a = BDD Node.Node
  deriving (BDD a -> BDD a -> Bool
(BDD a -> BDD a -> Bool) -> (BDD a -> BDD a -> Bool) -> Eq (BDD a)
forall a. BDD a -> BDD a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BDD a -> BDD a -> Bool
$c/= :: forall a. BDD a -> BDD a -> Bool
== :: BDD a -> BDD a -> Bool
$c== :: forall a. BDD a -> BDD a -> Bool
Eq, Int -> BDD a -> Int
BDD a -> Int
(Int -> BDD a -> Int) -> (BDD a -> Int) -> Hashable (BDD a)
forall a. Int -> BDD a -> Int
forall a. BDD a -> Int
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: BDD a -> Int
$chash :: forall a. BDD a -> Int
hashWithSalt :: Int -> BDD a -> Int
$chashWithSalt :: forall a. Int -> BDD a -> Int
Hashable)

pattern F :: BDD a
pattern $bF :: BDD a
$mF :: forall r a. BDD a -> (Void# -> r) -> (Void# -> r) -> r
F = BDD Node.F

pattern T :: BDD a
pattern $bT :: BDD a
$mT :: forall r a. BDD a -> (Void# -> r) -> (Void# -> r) -> r
T = BDD Node.T

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

{-# COMPLETE T, F, Branch #-}

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

data BDDCase2 a
  = BDDCase2LT Int (BDD a) (BDD a)
  | BDDCase2GT Int (BDD a) (BDD a)
  | BDDCase2EQ Int (BDD a) (BDD a) (BDD a) (BDD a)
  | BDDCase2EQ2 Bool Bool

bddCase2 :: forall a. ItemOrder a => Proxy a -> BDD a -> BDD a -> BDDCase2 a
bddCase2 :: Proxy a -> BDD a -> BDD a -> BDDCase2 a
bddCase2 Proxy a
_ (Branch Int
ptop BDD a
p0 BDD a
p1) (Branch Int
qtop BDD a
q0 BDD 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 -> BDD a -> BDD a -> BDDCase2 a
forall a. Int -> BDD a -> BDD a -> BDDCase2 a
BDDCase2LT Int
ptop BDD a
p0 BDD a
p1
    Ordering
GT -> Int -> BDD a -> BDD a -> BDDCase2 a
forall a. Int -> BDD a -> BDD a -> BDDCase2 a
BDDCase2GT Int
qtop BDD a
q0 BDD a
q1
    Ordering
EQ -> Int -> BDD a -> BDD a -> BDD a -> BDD a -> BDDCase2 a
forall a. Int -> BDD a -> BDD a -> BDD a -> BDD a -> BDDCase2 a
BDDCase2EQ Int
ptop BDD a
p0 BDD a
p1 BDD a
q0 BDD a
q1
bddCase2 Proxy a
_ (Branch Int
ptop BDD a
p0 BDD a
p1) BDD a
_ = Int -> BDD a -> BDD a -> BDDCase2 a
forall a. Int -> BDD a -> BDD a -> BDDCase2 a
BDDCase2LT Int
ptop BDD a
p0 BDD a
p1
bddCase2 Proxy a
_ BDD a
_ (Branch Int
qtop BDD a
q0 BDD a
q1) = Int -> BDD a -> BDD a -> BDDCase2 a
forall a. Int -> BDD a -> BDD a -> BDDCase2 a
BDDCase2GT Int
qtop BDD a
q0 BDD a
q1
bddCase2 Proxy a
_ BDD a
T BDD a
T = Bool -> Bool -> BDDCase2 a
forall a. Bool -> Bool -> BDDCase2 a
BDDCase2EQ2 Bool
True Bool
True
bddCase2 Proxy a
_ BDD a
T BDD a
F = Bool -> Bool -> BDDCase2 a
forall a. Bool -> Bool -> BDDCase2 a
BDDCase2EQ2 Bool
True Bool
False
bddCase2 Proxy a
_ BDD a
F BDD a
T = Bool -> Bool -> BDDCase2 a
forall a. Bool -> Bool -> BDDCase2 a
BDDCase2EQ2 Bool
False Bool
True
bddCase2 Proxy a
_ BDD a
F BDD a
F = Bool -> Bool -> BDDCase2 a
forall a. Bool -> Bool -> BDDCase2 a
BDDCase2EQ2 Bool
False Bool
False

level :: BDD a -> Level a
level :: BDD a -> Level a
level BDD a
T = Level a
forall a. Level a
Terminal
level BDD a
F = Level a
forall a. Level a
Terminal
level (Branch Int
x BDD a
_ BDD a
_) = Int -> Level a
forall a. Int -> Level a
NonTerminal Int
x

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

instance Show (BDD a) where
  showsPrec :: Int -> BDD a -> ShowS
showsPrec Int
d BDD 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 (BDD a -> (Graph, Int)
forall a. BDD a -> (Graph, Int)
toGraph BDD a
a)

instance Read (BDD a) where
  readPrec :: ReadPrec (BDD a)
readPrec = ReadPrec (BDD a) -> ReadPrec (BDD a)
forall a. ReadPrec a -> ReadPrec a
parens (ReadPrec (BDD a) -> ReadPrec (BDD a))
-> ReadPrec (BDD a) -> ReadPrec (BDD a)
forall a b. (a -> b) -> a -> b
$ Int -> ReadPrec (BDD a) -> ReadPrec (BDD a)
forall a. Int -> ReadPrec a -> ReadPrec a
prec Int
10 (ReadPrec (BDD a) -> ReadPrec (BDD a))
-> ReadPrec (BDD a) -> ReadPrec (BDD 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
    BDD a -> ReadPrec (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Graph, Int) -> BDD a
forall a. (Graph, Int) -> BDD a
fromGraph (Graph, Int)
gv)

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

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

-- | True
true :: BDD a
true :: BDD a
true = BDD a
forall a. BDD a
T

-- | False
false :: BDD a
false :: BDD a
false = BDD a
forall a. BDD a
F

-- | A variable \(x_i\)
var :: Int -> BDD a
var :: Int -> BDD a
var Int
ind = Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind BDD a
forall a. BDD a
F BDD a
forall a. BDD a
T

-- | Negation of a boolean function
notB :: BDD a -> BDD a
notB :: BDD a -> BDD a
notB BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s (BDD a)
f BDD a
T = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
F
      f BDD a
F = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
T
      f n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD 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) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) (BDD a -> ST s (BDD a)
f BDD a
lo) (BDD a -> ST s (BDD a)
f BDD a
hi)
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD 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) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  BDD a -> ST s (BDD a)
f BDD a
bdd

apply :: forall a. ItemOrder a => Bool -> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a
apply :: Bool
-> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a
apply Bool
isCommutative BDD a -> BDD a -> Maybe (BDD a)
func BDD a
bdd1 BDD a
bdd2 = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
op <- Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s.
ItemOrder a =>
Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
mkApplyOp Bool
isCommutative BDD a -> BDD a -> Maybe (BDD a)
func
  BDD a -> BDD a -> ST s (BDD a)
op BDD a
bdd1 BDD a
bdd2

mkApplyOp :: forall a s. ItemOrder a => Bool -> (BDD a -> BDD a -> Maybe (BDD a)) -> ST s (BDD a -> BDD a -> ST s (BDD a))
mkApplyOp :: Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
mkApplyOp Bool
isCommutative BDD a -> BDD a -> Maybe (BDD a)
func = do
  HashTable s (BDD a, BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a, BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> BDD a -> ST s (BDD a)
f BDD a
a BDD a
b | Just BDD a
c <- BDD a -> BDD a -> Maybe (BDD a)
func BDD a
a BDD a
b = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
c
      f BDD a
n1 BDD a
n2 = do
        let key :: (BDD a, BDD a)
key = if Bool
isCommutative Bool -> Bool -> Bool
&& BDD a -> Int
forall a. BDD a -> Int
nodeId BDD a
n2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< BDD a -> Int
forall a. BDD a -> Int
nodeId BDD a
n1 then (BDD a
n2, BDD a
n1) else (BDD a
n1, BDD a
n2)
        Maybe (BDD a)
m <- HashTable s (BDD a, BDD a) (BDD a)
-> (BDD a, BDD a) -> ST s (Maybe (BDD 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, BDD a) (BDD a)
h (BDD a, BDD a)
key
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- case Proxy a -> BDD a -> BDD a -> BDDCase2 a
forall a. ItemOrder a => Proxy a -> BDD a -> BDD a -> BDDCase2 a
bddCase2 (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) BDD a
n1 BDD a
n2 of
              BDDCase2GT Int
x2 BDD a
lo2 BDD a
hi2 -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
n1 BDD a
lo2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
n1 BDD a
hi2)
              BDDCase2LT Int
x1 BDD a
lo1 BDD a
hi1 -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x1) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo1 BDD a
n2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
hi1 BDD a
n2)
              BDDCase2EQ Int
x BDD a
lo1 BDD a
hi1 BDD a
lo2 BDD a
hi2 -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo1 BDD a
lo2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
hi1 BDD a
hi2)
              BDDCase2EQ2 Bool
_ Bool
_ -> String -> ST s (BDD a)
forall a. HasCallStack => String -> a
error String
"apply: should not happen"
            HashTable s (BDD a, BDD a) (BDD a)
-> (BDD a, BDD a) -> BDD 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, BDD a) (BDD a)
h (BDD a, BDD a)
key BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  (BDD a -> BDD a -> ST s (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a -> BDD a -> ST s (BDD a)
f

-- | Conjunction of two boolean function
(.&&.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.&&. :: BDD a -> BDD a -> BDD a
(.&&.) BDD a
bdd1 BDD a
bdd2 = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
op <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkAndOp
  BDD a -> BDD a -> ST s (BDD a)
op BDD a
bdd1 BDD a
bdd2

mkAndOp :: forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkAndOp :: ST s (BDD a -> BDD a -> ST s (BDD a))
mkAndOp = Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s.
ItemOrder a =>
Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
mkApplyOp Bool
True BDD a -> BDD a -> Maybe (BDD a)
forall a. BDD a -> BDD a -> Maybe (BDD a)
f
  where
    f :: BDD a -> BDD a -> Maybe (BDD a)
f BDD a
T BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
b
    f BDD a
F BDD a
_ = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
F
    f BDD a
a BDD a
T = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
a
    f BDD a
_ BDD a
F = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
F
    f BDD a
a BDD a
b | BDD a
a BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
a
    f BDD a
_ BDD a
_ = Maybe (BDD a)
forall a. Maybe a
Nothing

-- | Disjunction of two boolean function
(.||.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.||. :: BDD a -> BDD a -> BDD a
(.||.) BDD a
bdd1 BDD a
bdd2 = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
op <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkOrOp
  BDD a -> BDD a -> ST s (BDD a)
op BDD a
bdd1 BDD a
bdd2

mkOrOp :: forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkOrOp :: ST s (BDD a -> BDD a -> ST s (BDD a))
mkOrOp = Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s.
ItemOrder a =>
Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
mkApplyOp Bool
True BDD a -> BDD a -> Maybe (BDD a)
forall a. BDD a -> BDD a -> Maybe (BDD a)
f
  where
    f :: BDD a -> BDD a -> Maybe (BDD a)
f BDD a
T BDD a
_ = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
F BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
b
    f BDD a
_ BDD a
T = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
a BDD a
F = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
a
    f BDD a
a BDD a
b | BDD a
a BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
a
    f BDD a
_ BDD a
_ = Maybe (BDD a)
forall a. Maybe a
Nothing

-- | XOR
xor :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a
xor :: BDD a -> BDD a -> BDD a
xor BDD a
bdd1 BDD a
bdd2 = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
op <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkXOROp
  BDD a -> BDD a -> ST s (BDD a)
op BDD a
bdd1 BDD a
bdd2

mkXOROp :: forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkXOROp :: ST s (BDD a -> BDD a -> ST s (BDD a))
mkXOROp = Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s.
ItemOrder a =>
Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
mkApplyOp Bool
True BDD a -> BDD a -> Maybe (BDD a)
forall a. BDD a -> BDD a -> Maybe (BDD a)
f
  where
    f :: BDD a -> BDD a -> Maybe (BDD a)
f BDD a
F BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
b
    f BDD a
a BDD a
F = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
a
    f BDD a
a BDD a
b | BDD a
a BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
F
    f BDD a
_ BDD a
_ = Maybe (BDD a)
forall a. Maybe a
Nothing

-- | Implication
(.=>.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.=>. :: BDD a -> BDD a -> BDD a
(.=>.) = Bool
-> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a
forall a.
ItemOrder a =>
Bool
-> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a
apply Bool
False BDD a -> BDD a -> Maybe (BDD a)
forall a. BDD a -> BDD a -> Maybe (BDD a)
f
  where
    f :: BDD a -> BDD a -> Maybe (BDD a)
f BDD a
F BDD a
_ = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
T BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
b
    f BDD a
_ BDD a
T = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
a BDD a
b | BDD a
a BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
_ BDD a
_ = Maybe (BDD a)
forall a. Maybe a
Nothing

-- | Equivalence
(.<=>.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.<=>. :: BDD a -> BDD a -> BDD a
(.<=>.) = Bool
-> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a
forall a.
ItemOrder a =>
Bool
-> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a
apply Bool
True BDD a -> BDD a -> Maybe (BDD a)
forall a a. BDD a -> BDD a -> Maybe (BDD a)
f
  where
    f :: BDD a -> BDD a -> Maybe (BDD a)
f BDD a
T BDD a
T = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
T BDD a
F = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
F
    f BDD a
F BDD a
T = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
F
    f BDD a
F BDD a
F = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
a BDD a
b | BDD a
a BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
_ BDD a
_ = Maybe (BDD a)
forall a. Maybe a
Nothing

-- | If-then-else
ite :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a -> BDD a
ite :: BDD a -> BDD a -> BDD a -> BDD a
ite BDD a
c' BDD a
t' BDD a
e' = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a, BDD a, BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a, BDD a, BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
T BDD a
t BDD a
_ = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
t
      f BDD a
F BDD a
_ BDD a
e = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
e
      f BDD a
_ BDD a
t BDD a
e | BDD a
t BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
e = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
t
      f BDD a
c BDD a
t BDD a
e = do
        case [Level a] -> Level a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [BDD a -> Level a
forall a. BDD a -> Level a
level BDD a
c, BDD a -> Level a
forall a. BDD a -> Level a
level BDD a
t, BDD a -> Level a
forall a. BDD a -> Level a
level BDD a
e] of
          Level a
Terminal -> String -> ST s (BDD a)
forall a. HasCallStack => String -> a
error String
"should not happen"
          NonTerminal Int
x -> do
            let key :: (BDD a, BDD a, BDD a)
key = (BDD a
c, BDD a
t, BDD a
e)
            Maybe (BDD a)
m <- HashTable s (BDD a, BDD a, BDD a) (BDD a)
-> (BDD a, BDD a, BDD a) -> ST s (Maybe (BDD 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, BDD a, BDD a) (BDD a)
h (BDD a, BDD a, BDD a)
key
            case Maybe (BDD a)
m of
              Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
              Maybe (BDD a)
Nothing -> do
                let (BDD a
c0, BDD a
c1) = case BDD a
c of{ Branch Int
x' BDD a
lo BDD a
hi | Int
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x -> (BDD a
lo, BDD a
hi); BDD a
_ -> (BDD a
c, BDD a
c) }
                    (BDD a
t0, BDD a
t1) = case BDD a
t of{ Branch Int
x' BDD a
lo BDD a
hi | Int
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x -> (BDD a
lo, BDD a
hi); BDD a
_ -> (BDD a
t, BDD a
t) }
                    (BDD a
e0, BDD a
e1) = case BDD a
e of{ Branch Int
x' BDD a
lo BDD a
hi | Int
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x -> (BDD a
lo, BDD a
hi); BDD a
_ -> (BDD a
e, BDD a
e) }
                BDD a
ret <- (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x) (BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
c0 BDD a
t0 BDD a
e0) (BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
c1 BDD a
t1 BDD a
e1)
                HashTable s (BDD a, BDD a, BDD a) (BDD a)
-> (BDD a, BDD a, BDD a) -> BDD 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, BDD a, BDD a) (BDD a)
h (BDD a, BDD a, BDD a)
key BDD a
ret
                BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
c' BDD a
t' BDD a
e'

-- | Conjunction of a list of BDDs.
andB :: forall f a. (Foldable f, ItemOrder a) => f (BDD a) -> BDD a
andB :: f (BDD a) -> BDD a
andB f (BDD a)
xs = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
op <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkAndOp
  (BDD a -> BDD a -> ST s (BDD a))
-> BDD a -> f (BDD a) -> ST s (BDD a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM BDD a -> BDD a -> ST s (BDD a)
op BDD a
forall a. BDD a
true f (BDD a)
xs

-- | Disjunction of a list of BDDs.
orB :: forall f a. (Foldable f, ItemOrder a) => f (BDD a) -> BDD a
orB :: f (BDD a) -> BDD a
orB f (BDD a)
xs = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
op <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkOrOp
  (BDD a -> BDD a -> ST s (BDD a))
-> BDD a -> f (BDD a) -> ST s (BDD a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM BDD a -> BDD a -> ST s (BDD a)
op BDD a
forall a. BDD a
false f (BDD a)
xs

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

-- | Universal quantification (∀)
forAll :: forall a. ItemOrder a => Int -> BDD a -> BDD a
forAll :: Int -> BDD a -> BDD a
forAll Int
x BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
andOp <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkAndOp
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s (BDD a)
f n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD 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) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- if Int
ind Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x
                   then BDD a -> BDD a -> ST s (BDD a)
andOp BDD a
lo BDD a
hi
                   else (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) (BDD a -> ST s (BDD a)
f BDD a
lo) (BDD a -> ST s (BDD a)
f BDD a
hi)
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD 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) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
      f BDD a
a = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
a
  BDD a -> ST s (BDD a)
f BDD a
bdd

-- | Existential quantification (∃)
exists :: forall a. ItemOrder a => Int -> BDD a -> BDD a
exists :: Int -> BDD a -> BDD a
exists Int
x BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
orOp <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkOrOp
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s (BDD a)
f n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD 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) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- if Int
ind Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x
                   then BDD a -> BDD a -> ST s (BDD a)
orOp BDD a
lo BDD a
hi
                   else (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) (BDD a -> ST s (BDD a)
f BDD a
lo) (BDD a -> ST s (BDD a)
f BDD a
hi)
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD 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) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
      f BDD a
a = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
a
  BDD a -> ST s (BDD a)
f BDD a
bdd

-- | Unique existential quantification (∃!)
existsUnique :: forall a. ItemOrder a => Int -> BDD a -> BDD a
existsUnique :: Int -> BDD a -> BDD a
existsUnique Int
x BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
xorOp <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkXOROp
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s (BDD a)
f n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD 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) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD 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
ind Int
x of
              Ordering
LT -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) (BDD a -> ST s (BDD a)
f BDD a
lo) (BDD a -> ST s (BDD a)
f BDD a
hi)
              Ordering
EQ -> BDD a -> BDD a -> ST s (BDD a)
xorOp BDD a
lo BDD a
hi
              Ordering
GT -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
F
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD 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) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
      f BDD a
_ = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
F
  BDD a -> ST s (BDD a)
f BDD a
bdd

-- | Universal quantification (∀) over a set of variables
forAllSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a
forAllSet :: IntSet -> BDD a -> BDD a
forAllSet IntSet
vars BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
andOp <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkAndOp
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: [Int] -> BDD a -> ST s (BDD a)
f xxs :: [Int]
xxs@(Int
x : [Int]
xs) n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD 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) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD 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
ind Int
x of
              Ordering
LT -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) ([Int] -> BDD a -> ST s (BDD a)
f [Int]
xxs BDD a
lo) ([Int] -> BDD a -> ST s (BDD a)
f [Int]
xxs BDD a
hi)
              Ordering
EQ -> do
                BDD a
r0 <- [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
lo
                BDD a
r1 <- [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
hi
                BDD a -> BDD a -> ST s (BDD a)
andOp BDD a
r0 BDD a
r1
              Ordering
GT -> [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
n
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD 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) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
      f [Int]
_ BDD a
a = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
a
  [Int] -> BDD a -> ST s (BDD 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
vars)) BDD a
bdd

-- | Existential quantification (∃) over a set of variables
existsSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a
existsSet :: IntSet -> BDD a -> BDD a
existsSet IntSet
vars BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
orOp <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkOrOp
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: [Int] -> BDD a -> ST s (BDD a)
f xxs :: [Int]
xxs@(Int
x : [Int]
xs) n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD 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) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD 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
ind Int
x of
              Ordering
LT -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) ([Int] -> BDD a -> ST s (BDD a)
f [Int]
xxs BDD a
lo) ([Int] -> BDD a -> ST s (BDD a)
f [Int]
xxs BDD a
hi)
              Ordering
EQ -> do
                BDD a
r0 <- [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
lo
                BDD a
r1 <- [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
hi
                BDD a -> BDD a -> ST s (BDD a)
orOp BDD a
r0 BDD a
r1
              Ordering
GT -> [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
n
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD 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) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
      f [Int]
_ BDD a
a = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
a
  [Int] -> BDD a -> ST s (BDD 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
vars)) BDD a
bdd

-- | Unique existential quantification (∃!) over a set of variables
existsUniqueSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a
existsUniqueSet :: IntSet -> BDD a -> BDD a
existsUniqueSet IntSet
vars BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
xorOp <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkXOROp
  HashTable s ([Int], BDD a) (BDD a)
h <- Int -> ST s (HashTable s ([Int], BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: [Int] -> BDD a -> ST s (BDD a)
f xxs :: [Int]
xxs@(Int
x : [Int]
xs) n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        let key :: ([Int], BDD a)
key = ([Int]
xxs, BDD a
n)
        Maybe (BDD a)
m <- HashTable s ([Int], BDD a) (BDD a)
-> ([Int], BDD a) -> ST s (Maybe (BDD 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 ([Int], BDD a) (BDD a)
h ([Int], BDD a)
key
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD 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
ind Int
x of
              Ordering
LT -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) ([Int] -> BDD a -> ST s (BDD a)
f [Int]
xxs BDD a
lo) ([Int] -> BDD a -> ST s (BDD a)
f [Int]
xxs BDD a
hi)
              Ordering
EQ -> do
                BDD a
r0 <- [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
lo
                BDD a
r1 <- [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
hi
                BDD a -> BDD a -> ST s (BDD a)
xorOp BDD a
r0 BDD a
r1
              Ordering
GT -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
F
            HashTable s ([Int], BDD a) (BDD a)
-> ([Int], BDD a) -> BDD 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 ([Int], BDD a) (BDD a)
h ([Int], BDD a)
key BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
      f (Int
_ : [Int]
_) BDD a
_ = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
F
      f [] BDD a
a = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
a
  [Int] -> BDD a -> ST s (BDD 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
vars)) BDD a
bdd

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

-- | Fold over the graph structure of the BDD.
--
-- It takes values for substituting 'false' ('F') and 'true' ('T'),
-- and a function for substiting non-terminal node ('Branch').
fold :: b -> b -> (Int -> b -> b -> b) -> BDD a -> b
fold :: b -> b -> (Int -> b -> b -> b) -> BDD a -> b
fold b
ff b
tt Int -> b -> b -> b
br BDD a
bdd = (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 (BDD a) b
h <- Int -> ST s (HashTable s (BDD a) b)
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s b
f BDD a
F = b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
ff
      f BDD a
T = b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
tt
      f p :: BDD a
p@(Branch Int
top BDD a
lo BDD a
hi) = do
        Maybe b
m <- HashTable s (BDD a) b -> BDD 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 (BDD a) b
h BDD 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 <- BDD a -> ST s b
f BDD a
lo
            b
r1 <- BDD a -> ST s b
f BDD a
hi
            let ret :: b
ret = Int -> b -> b -> b
br Int
top b
r0 b
r1
            HashTable s (BDD a) b -> BDD 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 (BDD a) b
h BDD a
p b
ret
            b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
ret
  BDD a -> ST s b
f BDD a
bdd

-- | Strict version of 'fold'
fold' :: b -> b -> (Int -> b -> b -> b) -> BDD a -> b
fold' :: b -> b -> (Int -> b -> b -> b) -> BDD a -> b
fold' b
ff b
tt Int -> b -> b -> b
br BDD a
bdd = (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
  BDD a -> ST s b
op <- b -> b -> (Int -> b -> b -> b) -> ST s (BDD a -> ST s b)
forall b s a.
b -> b -> (Int -> b -> b -> b) -> ST s (BDD a -> ST s b)
mkFold'Op b
ff b
tt Int -> b -> b -> b
br
  BDD a -> ST s b
op BDD a
bdd

mkFold'Op :: b -> b -> (Int -> b -> b -> b) -> ST s (BDD a -> ST s b)
mkFold'Op :: b -> b -> (Int -> b -> b -> b) -> ST s (BDD a -> ST s b)
mkFold'Op !b
ff !b
tt Int -> b -> b -> b
br = do
  HashTable s (BDD a) b
h <- Int -> ST s (HashTable s (BDD a) b)
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s b
f BDD a
F = b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
ff
      f BDD a
T = b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
tt
      f p :: BDD a
p@(Branch Int
top BDD a
lo BDD a
hi) = do
        Maybe b
m <- HashTable s (BDD a) b -> BDD 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 (BDD a) b
h BDD 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 <- BDD a -> ST s b
f BDD a
lo
            b
r1 <- BDD a -> ST s b
f BDD a
hi
            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 (BDD a) b -> BDD 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 (BDD a) b
h BDD a
p b
ret
            b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
ret
  (BDD a -> ST s b) -> ST s (BDD a -> ST s b)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a -> ST s b
f

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

-- | All the variables that this BDD depends on.
support :: BDD a -> IntSet
support :: BDD a -> IntSet
support BDD a
bdd = (forall s. ST s IntSet) -> IntSet
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s IntSet) -> IntSet)
-> (forall s. ST s IntSet) -> IntSet
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> ST s IntSet
op <- ST s (BDD a -> ST s IntSet)
forall s a. ST s (BDD a -> ST s IntSet)
mkSupportOp
  BDD a -> ST s IntSet
op BDD a
bdd

mkSupportOp :: ST s (BDD a -> ST s IntSet)
mkSupportOp :: ST s (BDD a -> ST s IntSet)
mkSupportOp = IntSet
-> IntSet
-> (Int -> IntSet -> IntSet -> IntSet)
-> ST s (BDD a -> ST s IntSet)
forall b s a.
b -> b -> (Int -> b -> b -> b) -> ST s (BDD a -> ST s b)
mkFold'Op IntSet
IntSet.empty IntSet
IntSet.empty Int -> IntSet -> IntSet -> IntSet
f
  where
    f :: Int -> IntSet -> IntSet -> IntSet
f Int
x IntSet
lo IntSet
hi = Int -> IntSet -> IntSet
IntSet.insert Int
x (IntSet
lo IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
hi)

-- | Evaluate a boolean function represented as BDD under the valuation
-- given by @(Int -> Bool)@, i.e. it lifts a valuation function from
-- variables to BDDs.
evaluate :: (Int -> Bool) -> BDD a -> Bool
evaluate :: (Int -> Bool) -> BDD a -> Bool
evaluate Int -> Bool
f = BDD a -> Bool
forall a. BDD a -> Bool
g
  where
    g :: BDD a -> Bool
g BDD a
F = Bool
False
    g BDD a
T = Bool
True
    g (Branch Int
x BDD a
lo BDD a
hi)
      | Int -> Bool
f Int
x = BDD a -> Bool
g BDD a
hi
      | Bool
otherwise = BDD a -> Bool
g BDD a
lo

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

-- | Compute \(F_x \) or \(F_{\neg x} \).
restrict :: forall a. ItemOrder a => Int -> Bool -> BDD a -> BDD a
restrict :: Int -> Bool -> BDD a -> BDD a
restrict Int
x Bool
val BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s (BDD a)
f BDD a
T = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
T
      f BDD a
F = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
F
      f n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD 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) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD 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
ind Int
x of
              Ordering
GT -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
n
              Ordering
LT -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) (BDD a -> ST s (BDD a)
f BDD a
lo) (BDD a -> ST s (BDD a)
f BDD a
hi)
              Ordering
EQ -> if Bool
val then BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
hi else BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
lo
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD 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) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  BDD a -> ST s (BDD a)
f BDD a
bdd

-- | Compute \(F_{\{x_i = v_i\}_i} \).
restrictSet :: forall a. ItemOrder a => IntMap Bool -> BDD a -> BDD a
restrictSet :: IntMap Bool -> BDD a -> BDD a
restrictSet IntMap Bool
val BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: [(Int, Bool)] -> BDD a -> ST s (BDD a)
f [] BDD a
n = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
n
      f [(Int, Bool)]
_ BDD a
T = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
T
      f [(Int, Bool)]
_ BDD a
F = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
F
      f xxs :: [(Int, Bool)]
xxs@((Int
x,Bool
v) : [(Int, Bool)]
xs) n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD 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) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD 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
ind Int
x of
              Ordering
GT -> [(Int, Bool)] -> BDD a -> ST s (BDD a)
f [(Int, Bool)]
xs BDD a
n
              Ordering
LT -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) ([(Int, Bool)] -> BDD a -> ST s (BDD a)
f [(Int, Bool)]
xxs BDD a
lo) ([(Int, Bool)] -> BDD a -> ST s (BDD a)
f [(Int, Bool)]
xxs BDD a
hi)
              Ordering
EQ -> if Bool
v then [(Int, Bool)] -> BDD a -> ST s (BDD a)
f [(Int, Bool)]
xs BDD a
hi else [(Int, Bool)] -> BDD a -> ST s (BDD a)
f [(Int, Bool)]
xs BDD a
lo
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD 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) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  [(Int, Bool)] -> BDD a -> ST s (BDD a)
f (((Int, Bool) -> (Int, Bool) -> Ordering)
-> [(Int, Bool)] -> [(Int, Bool)]
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 -> Ordering)
-> ((Int, Bool) -> Int) -> (Int, Bool) -> (Int, Bool) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, Bool) -> Int
forall a b. (a, b) -> a
fst) (IntMap Bool -> [(Int, Bool)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Bool
val)) BDD a
bdd

-- | Compute generalized cofactor of F with respect to C.
--
-- Note that C is the first argument.
restrictLaw :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a
restrictLaw :: BDD a -> BDD a -> BDD a
restrictLaw BDD a
law BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a, BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a, BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> BDD a -> ST s (BDD a)
f BDD a
T BDD a
n = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
n
      f BDD a
F BDD a
_ = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
T  -- Is this correct?
      f BDD a
_ BDD a
F = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
F
      f BDD a
_ BDD a
T = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
T
      f BDD a
n1 BDD a
n2 | BDD a
n1 BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
n2 = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
T
      f BDD a
n1 BDD a
n2 = do
        Maybe (BDD a)
m <- HashTable s (BDD a, BDD a) (BDD a)
-> (BDD a, BDD a) -> ST s (Maybe (BDD 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, BDD a) (BDD a)
h (BDD a
n1, BDD a
n2)
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- case Proxy a -> BDD a -> BDD a -> BDDCase2 a
forall a. ItemOrder a => Proxy a -> BDD a -> BDD a -> BDDCase2 a
bddCase2 (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) BDD a
n1 BDD a
n2 of
              BDDCase2GT Int
x2 BDD a
lo2 BDD a
hi2 -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
n1 BDD a
lo2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
n1 BDD a
hi2)
              BDDCase2EQ Int
x1 BDD a
lo1 BDD a
hi1 BDD a
lo2 BDD a
hi2
                | BDD a
lo1 BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
forall a. BDD a
F  -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
hi1 BDD a
hi2
                | BDD a
hi1 BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
forall a. BDD a
F  -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo1 BDD a
lo2
                | Bool
otherwise -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x1) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo1 BDD a
lo2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
hi1 BDD a
hi2)
              BDDCase2LT Int
x1 BDD a
lo1 BDD a
hi1
                | BDD a
lo1 BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
forall a. BDD a
F  -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
hi1 BDD a
n2
                | BDD a
hi1 BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
forall a. BDD a
F  -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo1 BDD a
n2
                | Bool
otherwise -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x1) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo1 BDD a
n2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
hi1 BDD a
n2)
              BDDCase2EQ2 Bool
_ Bool
_ -> String -> ST s (BDD a)
forall a. HasCallStack => String -> a
error String
"restrictLaw: should not happen"
            HashTable s (BDD a, BDD a) (BDD a)
-> (BDD a, BDD a) -> BDD 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, BDD a) (BDD a)
h (BDD a
n1, BDD a
n2) BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  BDD a -> BDD a -> ST s (BDD a)
f BDD a
law BDD a
bdd

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

-- | @subst x N M@ computes substitution \(M_{x = N}\).
--
-- This operation is also known as /Composition/.
subst :: forall a. ItemOrder a => Int -> BDD a -> BDD a -> BDD a
subst :: Int -> BDD a -> BDD a -> BDD a
subst Int
x BDD a
n BDD a
m = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a, BDD a, BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a, BDD a, BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> BDD a -> BDD a -> ST s (BDD a)
f (Branch Int
x' BDD a
lo BDD a
_) BDD a
mhi BDD a
n2 | Int
xInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
x' = BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo BDD a
mhi BDD a
n2
      f BDD a
mlo (Branch Int
x' BDD a
_ BDD a
hi) BDD a
n2 | Int
xInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
x' = BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
mlo BDD a
hi BDD a
n2
      f BDD a
mlo BDD a
_ BDD a
F = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return (BDD a -> ST s (BDD a)) -> BDD a -> ST s (BDD a)
forall a b. (a -> b) -> a -> b
$ Int -> Bool -> BDD a -> BDD a
forall a. ItemOrder a => Int -> Bool -> BDD a -> BDD a
restrict Int
x Bool
False BDD a
mlo
      f BDD a
_ BDD a
mhi BDD a
T = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return (BDD a -> ST s (BDD a)) -> BDD a -> ST s (BDD a)
forall a b. (a -> b) -> a -> b
$ Int -> Bool -> BDD a -> BDD a
forall a. ItemOrder a => Int -> Bool -> BDD a -> BDD a
restrict Int
x Bool
True BDD a
mhi
      f BDD a
mlo BDD a
mhi BDD a
n2 = do
        Maybe (BDD a)
u <- HashTable s (BDD a, BDD a, BDD a) (BDD a)
-> (BDD a, BDD a, BDD a) -> ST s (Maybe (BDD 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, BDD a, BDD a) (BDD a)
h (BDD a
mlo, BDD a
mhi, BDD a
n2)
        case Maybe (BDD a)
u of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            case [Level a] -> Level a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ((BDD a -> Level a) -> [BDD a] -> [Level a]
forall a b. (a -> b) -> [a] -> [b]
map BDD a -> Level a
forall a. BDD a -> Level a
level [BDD a
mlo, BDD a
mhi, BDD a
n2]) of
              Level a
Terminal -> String -> ST s (BDD a)
forall a. HasCallStack => String -> a
error String
"should not happen"
              NonTerminal Int
x' -> do
                let (BDD a
mll, BDD a
mlh) =
                      case BDD a
mlo of
                        Branch Int
x'' BDD a
mll' BDD a
mlh' | Int
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x'' -> (BDD a
mll', BDD a
mlh')
                        BDD a
_ -> (BDD a
mlo, BDD a
mlo)
                    (BDD a
mhl, BDD a
mhh) =
                      case BDD a
mhi of
                        Branch Int
x'' BDD a
mhl' BDD a
mhh' | Int
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x'' -> (BDD a
mhl', BDD a
mhh')
                        BDD a
_ -> (BDD a
mhi, BDD a
mhi)
                    (BDD a
n2l, BDD a
n2h) =
                      case BDD a
n2 of
                        Branch Int
x'' BDD a
n2l' BDD a
n2h' | Int
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x'' -> (BDD a
n2l', BDD a
n2h')
                        BDD a
_ -> (BDD a
n2, BDD a
n2)
                BDD a
r0 <- BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
mll BDD a
mhl BDD a
n2l
                BDD a
r1 <- BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
mlh BDD a
mhh BDD a
n2h
                let ret :: BDD a
ret = Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x' BDD a
r0 BDD a
r1
                HashTable s (BDD a, BDD a, BDD a) (BDD a)
-> (BDD a, BDD a, BDD a) -> BDD 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, BDD a, BDD a) (BDD a)
h (BDD a
mlo, BDD a
mhi, BDD a
n2) BDD a
ret
                BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
m BDD a
m BDD a
n

-- | Simultaneous substitution
substSet :: forall a. ItemOrder a => IntMap (BDD a) -> BDD a -> BDD a
substSet :: IntMap (BDD a) -> BDD a -> BDD a
substSet IntMap (BDD a)
s BDD a
m = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> ST s IntSet
supportOp <- ST s (BDD a -> ST s IntSet)
forall s a. ST s (BDD a -> ST s IntSet)
mkSupportOp

  HashTable
  s
  ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
  (BDD a)
h <- Int
-> ST
     s
     (HashTable
        s
        ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
        (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let -- f :: IntMap (BDD a) -> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST _ (BDD a)
      f :: IntMap (BDD a)
-> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST s (BDD a)
f IntMap (BDD a)
conditions [(IntMap Bool, BDD a)]
conditioned IntMap (BDD a)
_ | Bool -> Bool -> Bool
forall a. HasCallStack => Bool -> a -> a
assert ([(IntMap Bool, BDD a)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(IntMap Bool, BDD a)]
conditioned Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1 Bool -> Bool -> Bool
&& ((IntMap Bool, BDD a) -> Bool) -> [(IntMap Bool, BDD a)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(IntMap Bool
cond, BDD a
_) -> IntMap Bool -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet IntMap Bool
cond IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` IntMap (BDD a) -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet IntMap (BDD a)
conditions) [(IntMap Bool, BDD a)]
conditioned) Bool
False = ST s (BDD a)
forall a. HasCallStack => a
undefined
      f IntMap (BDD a)
conditions [(IntMap Bool, BDD a)]
conditioned IntMap (BDD a)
remaining = do
        let l1 :: Level a
l1 = [Level a] -> Level a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Level a] -> Level a) -> [Level a] -> Level a
forall a b. (a -> b) -> a -> b
$ ((IntMap Bool, BDD a) -> Level a)
-> [(IntMap Bool, BDD a)] -> [Level a]
forall a b. (a -> b) -> [a] -> [b]
map (BDD a -> Level a
forall a. BDD a -> Level a
level (BDD a -> Level a)
-> ((IntMap Bool, BDD a) -> BDD a)
-> (IntMap Bool, BDD a)
-> Level a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntMap Bool, BDD a) -> BDD a
forall a b. (a, b) -> b
snd) [(IntMap Bool, BDD a)]
conditioned
            -- remaining' = IntMap.filterWithKey (\x _ -> l1 <= NonTerminal x) remaining
        IntMap (BDD a)
remaining' <- do
          IntSet
tmp <- ([IntSet] -> IntSet) -> ST s [IntSet] -> ST s IntSet
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions (ST s [IntSet] -> ST s IntSet) -> ST s [IntSet] -> ST s IntSet
forall a b. (a -> b) -> a -> b
$ ((IntMap Bool, BDD a) -> ST s IntSet)
-> [(IntMap Bool, BDD a)] -> ST s [IntSet]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (BDD a -> ST s IntSet
supportOp (BDD a -> ST s IntSet)
-> ((IntMap Bool, BDD a) -> BDD a)
-> (IntMap Bool, BDD a)
-> ST s IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntMap Bool, BDD a) -> BDD a
forall a b. (a, b) -> b
snd) [(IntMap Bool, BDD a)]
conditioned
          IntMap (BDD a) -> ST s (IntMap (BDD a))
forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap (BDD a) -> ST s (IntMap (BDD a)))
-> IntMap (BDD a) -> ST s (IntMap (BDD a))
forall a b. (a -> b) -> a -> b
$ IntMap (BDD a) -> IntSet -> IntMap (BDD a)
forall a. IntMap a -> IntSet -> IntMap a
IntMap.restrictKeys IntMap (BDD a)
remaining IntSet
tmp
        let l :: Level a
l = [Level a] -> Level a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Level a] -> Level a) -> [Level a] -> Level a
forall a b. (a -> b) -> a -> b
$ Level a
l1 Level a -> [Level a] -> [Level a]
forall a. a -> [a] -> [a]
: (BDD a -> Level a) -> [BDD a] -> [Level a]
forall a b. (a -> b) -> [a] -> [b]
map BDD a -> Level a
forall a. BDD a -> Level a
level (IntMap (BDD a) -> [BDD a]
forall a. IntMap a -> [a]
IntMap.elems IntMap (BDD a)
remaining' [BDD a] -> [BDD a] -> [BDD a]
forall a. [a] -> [a] -> [a]
++ IntMap (BDD a) -> [BDD a]
forall a. IntMap a -> [a]
IntMap.elems IntMap (BDD a)
conditions)
        Bool -> ST s () -> ST s ()
forall a. HasCallStack => Bool -> a -> a
assert ((Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Int
c -> Int -> Level a
forall a. Int -> Level a
NonTerminal Int
c Level a -> Level a -> Bool
forall a. Ord a => a -> a -> Bool
<= Level a
l) (IntMap (BDD a) -> [Int]
forall a. IntMap a -> [Int]
IntMap.keys IntMap (BDD a)
conditions)) (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ () -> ST s ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        case Level a
l of
          Level a
Terminal -> do
            case IntMap (BDD a)
-> [(IntMap Bool, BDD a)]
-> (IntMap (BDD a), [(IntMap Bool, BDD a)])
propagateFixed IntMap (BDD a)
conditions [(IntMap Bool, BDD a)]
conditioned of
              (IntMap (BDD a)
conditions', [(IntMap Bool, BDD a)]
conditioned') ->
                Bool -> ST s (BDD a) -> ST s (BDD a)
forall a. HasCallStack => Bool -> a -> a
assert (IntMap (BDD a) -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap (BDD a)
conditions' Bool -> Bool -> Bool
&& [(IntMap Bool, BDD a)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(IntMap Bool, BDD a)]
conditioned' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (ST s (BDD a) -> ST s (BDD a)) -> ST s (BDD a) -> ST s (BDD a)
forall a b. (a -> b) -> a -> b
$
                  BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((IntMap Bool, BDD a) -> BDD a
forall a b. (a, b) -> b
snd ([(IntMap Bool, BDD a)] -> (IntMap Bool, BDD a)
forall a. [a] -> a
head [(IntMap Bool, BDD a)]
conditioned'))
          NonTerminal Int
x
            | Level a
l Level a -> Level a -> Bool
forall a. Eq a => a -> a -> Bool
== Level a
l1 Bool -> Bool -> Bool
&& Int
x Int -> IntMap (BDD a) -> Bool
forall a. Int -> IntMap a -> Bool
`IntMap.member` IntMap (BDD a)
remaining' -> do
                let conditions' :: IntMap (BDD a)
conditions' = Int -> BDD a -> IntMap (BDD a) -> IntMap (BDD a)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x (IntMap (BDD a)
remaining' IntMap (BDD a) -> Int -> BDD a
forall a. IntMap a -> Int -> a
IntMap.! Int
x) IntMap (BDD a)
conditions
                    conditioned' :: [(IntMap Bool, BDD a)]
conditioned' = do
                      (IntMap Bool
cond, BDD a
a) <- [(IntMap Bool, BDD a)]
conditioned
                      case BDD a
a of
                        Branch Int
x' BDD a
lo BDD a
hi | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' -> [(Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
False IntMap Bool
cond, BDD a
lo), (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
True IntMap Bool
cond, BDD a
hi)]
                        BDD a
_ -> [(IntMap Bool
cond, BDD a
a)]
                IntMap (BDD a)
-> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST s (BDD a)
f IntMap (BDD a)
conditions' [(IntMap Bool, BDD a)]
conditioned' (Int -> IntMap (BDD a) -> IntMap (BDD a)
forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
x IntMap (BDD a)
remaining')
            | Bool
otherwise -> do
                case IntMap (BDD a)
-> [(IntMap Bool, BDD a)]
-> (IntMap (BDD a), [(IntMap Bool, BDD a)])
propagateFixed IntMap (BDD a)
conditions [(IntMap Bool, BDD a)]
conditioned of
                  (IntMap (BDD a)
conditions', [(IntMap Bool, BDD a)]
conditioned') -> do
                    let key :: ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
key = (IntMap (BDD a) -> [(Int, BDD a)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (BDD a)
conditions', [(IntMap Bool -> [(Int, Bool)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Bool
cond, BDD a
a) | (IntMap Bool
cond, BDD a
a) <- [(IntMap Bool, BDD a)]
conditioned'], IntMap (BDD a) -> [(Int, BDD a)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (BDD a)
remaining')  -- キーを減らせる?
                    Maybe (BDD a)
u <- HashTable
  s
  ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
  (BDD a)
-> ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
-> ST s (Maybe (BDD 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
  ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
  (BDD a)
h ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
key
                    case Maybe (BDD a)
u of
                      Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
                      Maybe (BDD a)
Nothing -> do
                        let f0 :: BDD a -> BDD a
f0 (Branch Int
x' BDD a
lo BDD a
_) | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' = BDD a
lo
                            f0 BDD a
a = BDD a
a
                            f1 :: BDD a -> BDD a
f1 (Branch Int
x' BDD a
_ BDD a
hi) | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' = BDD a
hi
                            f1 BDD a
a = BDD a
a
                        BDD a
r0 <- IntMap (BDD a)
-> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST s (BDD a)
f ((BDD a -> BDD a) -> IntMap (BDD a) -> IntMap (BDD a)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map BDD a -> BDD a
forall a. BDD a -> BDD a
f0 IntMap (BDD a)
conditions') [(IntMap Bool
cond, BDD a -> BDD a
forall a. BDD a -> BDD a
f0 BDD a
a) | (IntMap Bool
cond, BDD a
a) <- [(IntMap Bool, BDD a)]
conditioned'] ((BDD a -> BDD a) -> IntMap (BDD a) -> IntMap (BDD a)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map BDD a -> BDD a
forall a. BDD a -> BDD a
f0 IntMap (BDD a)
remaining')
                        BDD a
r1 <- IntMap (BDD a)
-> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST s (BDD a)
f ((BDD a -> BDD a) -> IntMap (BDD a) -> IntMap (BDD a)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map BDD a -> BDD a
forall a. BDD a -> BDD a
f1 IntMap (BDD a)
conditions') [(IntMap Bool
cond, BDD a -> BDD a
forall a. BDD a -> BDD a
f1 BDD a
a) | (IntMap Bool
cond, BDD a
a) <- [(IntMap Bool, BDD a)]
conditioned'] ((BDD a -> BDD a) -> IntMap (BDD a) -> IntMap (BDD a)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map BDD a -> BDD a
forall a. BDD a -> BDD a
f1 IntMap (BDD a)
remaining')
                        let ret :: BDD a
ret = Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x BDD a
r0 BDD a
r1
                        HashTable
  s
  ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
  (BDD a)
-> ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
-> BDD 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
  ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
  (BDD a)
h ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
key BDD a
ret
                        BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  IntMap (BDD a)
-> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST s (BDD a)
f IntMap (BDD a)
forall a. IntMap a
IntMap.empty [(IntMap Bool
forall a. IntMap a
IntMap.empty, BDD a
m)] IntMap (BDD a)
s

  where
    propagateFixed :: IntMap (BDD a) -> [(IntMap Bool, BDD a)] -> (IntMap (BDD a), [(IntMap Bool, BDD a)])
    propagateFixed :: IntMap (BDD a)
-> [(IntMap Bool, BDD a)]
-> (IntMap (BDD a), [(IntMap Bool, BDD a)])
propagateFixed IntMap (BDD a)
conditions [(IntMap Bool, BDD a)]
conditioned
      | IntMap Bool -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap Bool
fixed = (IntMap (BDD a)
conditions, [(IntMap Bool, BDD a)]
conditioned)
      | Bool
otherwise =
          ( IntMap (BDD a) -> IntMap Bool -> IntMap (BDD a)
forall a b. IntMap a -> IntMap b -> IntMap a
IntMap.difference IntMap (BDD a)
conditions IntMap Bool
fixed
          , [(IntMap Bool -> IntMap Bool -> IntMap Bool
forall a b. IntMap a -> IntMap b -> IntMap a
IntMap.difference IntMap Bool
cond IntMap Bool
fixed, BDD a
a) | (IntMap Bool
cond, BDD a
a) <- [(IntMap Bool, BDD a)]
conditioned, IntMap Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (IntMap Bool -> Bool) -> IntMap Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool -> Bool) -> IntMap Bool -> IntMap Bool -> IntMap Bool
forall a b c. (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IntMap.intersectionWith Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) IntMap Bool
fixed IntMap Bool
cond]
          )
      where
        fixed :: IntMap Bool
fixed = (BDD a -> Maybe Bool) -> IntMap (BDD a) -> IntMap Bool
forall a b. (a -> Maybe b) -> IntMap a -> IntMap b
IntMap.mapMaybe BDD a -> Maybe Bool
asBool IntMap (BDD a)
conditions

    asBool :: BDD a -> Maybe Bool
    asBool :: BDD a -> Maybe Bool
asBool BDD a
a =
      case BDD a
a of
        BDD a
T -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
        BDD a
F -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
        BDD a
_ -> Maybe Bool
forall a. Maybe a
Nothing

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

type Graph = IntMap Node

data Node
  = NodeF
  | NodeT
  | 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 BDD into a pointed graph
toGraph :: BDD a -> (Graph, Int)
toGraph :: BDD a -> (Graph, Int)
toGraph BDD a
bdd =
  case Identity (BDD a) -> (Graph, Identity Int)
forall (t :: * -> *) a.
Traversable t =>
t (BDD a) -> (Graph, t Int)
toGraph' (BDD a -> Identity (BDD a)
forall a. a -> Identity a
Identity BDD a
bdd) of
    (Graph
g, Identity Int
v) -> (Graph
g, Int
v)

-- | Convert multiple BDDs into a graph
toGraph' :: Traversable t => t (BDD a) -> (Graph, t Int)
toGraph' :: t (BDD a) -> (Graph, t Int)
toGraph' t (BDD 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 (BDD a) Int
h <- Int -> ST s (HashTable s (BDD a) Int)
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  HashTable s (BDD a) Int -> BDD 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 (BDD a) Int
h BDD a
forall a. BDD a
F Int
0
  HashTable s (BDD a) Int -> BDD 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 (BDD a) Int
h BDD a
forall a. BDD a
T 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
NodeF), (Int
1, Node
NodeT)]

  let f :: BDD a -> ST s Int
f BDD a
F = Int -> ST s Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
      f BDD a
T = Int -> ST s Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
      f p :: BDD a
p@(Branch Int
x BDD a
lo BDD a
hi) = do
        Maybe Int
m <- HashTable s (BDD a) Int -> BDD 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 (BDD a) Int
h BDD 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 <- BDD a -> ST s Int
f BDD a
lo
            Int
r1 <- BDD a -> ST s Int
f BDD 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 (BDD a) Int -> BDD 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 (BDD a) Int
h BDD 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 <- (BDD a -> ST s Int) -> t (BDD a) -> ST s (t Int)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM BDD a -> ST s Int
f t (BDD 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 BDD
fromGraph :: (Graph, Int) -> BDD a
fromGraph :: (Graph, Int) -> BDD a
fromGraph (Graph
g, Int
v) =
  case Int -> IntMap (BDD a) -> Maybe (BDD a)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
v (Graph -> IntMap (BDD a)
forall a. Graph -> IntMap (BDD a)
fromGraph' Graph
g) of
    Maybe (BDD a)
Nothing -> String -> BDD a
forall a. HasCallStack => String -> a
error (String
"Data.DecisionDiagram.BDD.fromGraph: invalid node id " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
v)
    Just BDD a
bdd -> BDD a
bdd

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

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

-- https://ja.wikipedia.org/wiki/%E4%BA%8C%E5%88%86%E6%B1%BA%E5%AE%9A%E5%9B%B3
_test_bdd :: BDD AscOrder
_test_bdd :: BDD AscOrder
_test_bdd = (BDD AscOrder -> BDD AscOrder
forall a. BDD a -> BDD a
notB BDD AscOrder
forall a. BDD a
x1 BDD AscOrder -> BDD AscOrder -> BDD AscOrder
forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.&&. BDD AscOrder -> BDD AscOrder
forall a. BDD a -> BDD a
notB BDD AscOrder
forall a. BDD a
x2 BDD AscOrder -> BDD AscOrder -> BDD AscOrder
forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.&&. BDD AscOrder -> BDD AscOrder
forall a. BDD a -> BDD a
notB BDD AscOrder
forall a. BDD a
x3) BDD AscOrder -> BDD AscOrder -> BDD AscOrder
forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.||. (BDD AscOrder
forall a. BDD a
x1 BDD AscOrder -> BDD AscOrder -> BDD AscOrder
forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.&&. BDD AscOrder
forall a. BDD a
x2) BDD AscOrder -> BDD AscOrder -> BDD AscOrder
forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.||. (BDD AscOrder
forall a. BDD a
x2 BDD AscOrder -> BDD AscOrder -> BDD AscOrder
forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.&&. BDD AscOrder
forall a. BDD a
x3)
  where
    x1 :: BDD a
x1 = Int -> BDD a
forall a. Int -> BDD a
var Int
1
    x2 :: BDD a
x2 = Int -> BDD a
forall a. Int -> BDD a
var Int
2
    x3 :: BDD a
x3 = Int -> BDD a
forall a. Int -> BDD a
var Int
3
{-
BDD (Node 880 (UBranch 1 (Node 611 (UBranch 2 (Node 836 UT) (Node 215 UF))) (Node 806 (UBranch 2 (Node 842 (UBranch 3 (Node 836 UT) (Node 215 UF))) (Node 464 (UBranch 3 (Node 215 UF) (Node 836 UT)))))))
-}

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