{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
module Data.DecisionDiagram.BDD
(
BDD (F, T, Branch)
, ItemOrder (..)
, AscOrder
, DescOrder
, withDefaultOrder
, withAscOrder
, withDescOrder
, withCustomOrder
, true
, false
, var
, notB
, (.&&.)
, (.||.)
, xor
, (.=>.)
, (.<=>.)
, ite
, andB
, orB
, forAll
, exists
, existsUnique
, forAllSet
, existsSet
, existsUniqueSet
, support
, evaluate
, restrict
, restrictSet
, restrictLaw
, subst
, substSet
, fold
, fold'
, 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
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
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 :: BDD a
true :: BDD a
true = BDD a
forall a. BDD a
T
false :: BDD a
false :: BDD a
false = BDD a
forall a. BDD a
F
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
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
(.&&.) :: 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
(.||.) :: 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 :: 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
(.=>.) :: 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
(.<=>.) :: 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
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'
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
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
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
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
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
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
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
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 :: 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
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
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 :: (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
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
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
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
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 :: 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
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 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
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)
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)
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)
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
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'
_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