{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
module Data.DecisionDiagram.BDD
(
BDD (Leaf, Branch)
, ItemOrder (..)
, AscOrder
, DescOrder
, withDefaultOrder
, withAscOrder
, withDescOrder
, withCustomOrder
, true
, false
, var
, notB
, (.&&.)
, (.||.)
, xor
, (.=>.)
, (.<=>.)
, ite
, andB
, orB
, pbAtLeast
, pbAtMost
, pbExactly
, pbExactlyIntegral
, forAll
, exists
, existsUnique
, forAllSet
, existsSet
, existsUniqueSet
, support
, evaluate
, numNodes
, restrict
, restrictSet
, restrictLaw
, subst
, substSet
, anySat
, allSat
, anySatComplete
, allSatComplete
, countSat
, uniformSatM
, Sig (..)
, inSig
, outSig
, fold
, fold'
, unfoldHashable
, unfoldOrd
, lfp
, gfp
, Graph
, toGraph
, toGraph'
, fromGraph
, fromGraph'
) where
import Control.Exception (assert)
import Control.Monad
#if !MIN_VERSION_mwc_random(0,15,0)
import Control.Monad.Primitive
#endif
import Control.Monad.ST
import Control.Monad.ST.Unsafe
import Data.Bits (Bits (shiftL))
import qualified Data.Foldable as Foldable
import Data.Function (on)
import Data.Hashable
import qualified Data.HashMap.Lazy as HashMap
import qualified Data.HashTable.Class as H
import qualified Data.HashTable.ST.Cuckoo as C
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.List (sortBy)
import Data.Map.Lazy (Map)
import qualified Data.Map.Lazy as Map
import Data.Proxy
import Data.Ratio
import qualified Data.Vector as V
import GHC.Stack
import Numeric.Natural
#if MIN_VERSION_mwc_random(0,15,0)
import System.Random.MWC (Uniform (..))
import System.Random.Stateful (StatefulGen (..))
#else
import System.Random.MWC (Gen, Variate (..))
#endif
import System.Random.MWC.Distributions (bernoulli)
import Text.Read
import Data.DecisionDiagram.BDD.Internal.ItemOrder
import Data.DecisionDiagram.BDD.Internal.Node (Sig (..), Graph)
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, Eq (BDD a)
Eq (BDD a)
-> (Int -> BDD a -> Int) -> (BDD a -> Int) -> Hashable (BDD a)
Int -> BDD a -> Int
BDD a -> Int
forall a. Eq (BDD a)
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall a. Int -> BDD a -> Int
forall a. BDD a -> Int
hash :: BDD a -> Int
$chash :: forall a. BDD a -> Int
hashWithSalt :: Int -> BDD a -> Int
$chashWithSalt :: forall a. Int -> BDD a -> Int
$cp1Hashable :: forall a. Eq (BDD a)
Hashable)
pattern F :: BDD a
pattern $bF :: BDD a
$mF :: forall r a. BDD a -> (Void# -> r) -> (Void# -> r) -> r
F = Leaf False
pattern T :: BDD a
pattern $bT :: BDD a
$mT :: forall r a. BDD a -> (Void# -> r) -> (Void# -> r) -> r
T = Leaf True
pattern Leaf :: Bool -> BDD a
pattern $bLeaf :: Bool -> BDD a
$mLeaf :: forall r a. BDD a -> (Bool -> r) -> (Void# -> r) -> r
Leaf b = BDD (Node.Leaf b)
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 #-}
{-# COMPLETE Leaf, 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
_ (Leaf Bool
b1) (Leaf Bool
b2) = Bool -> Bool -> BDDCase2 a
forall a. Bool -> Bool -> BDDCase2 a
BDDCase2EQ2 Bool
b1 Bool
b2
level :: BDD a -> Level a
level :: BDD a -> Level a
level (Branch Int
x BDD a
_ BDD a
_) = Int -> Level a
forall a. Int -> Level a
NonTerminal Int
x
level (Leaf Bool
_) = Level a
forall a. Level a
Terminal
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 Sig, Int) -> ShowS
forall a. Show a => a -> ShowS
shows (BDD a -> (Graph Sig, Int)
forall a. BDD a -> (Graph Sig, 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 Sig, Int)
gv <- ReadPrec (Graph Sig, Int)
forall a. Read a => ReadPrec a
readPrec
BDD a -> ReadPrec (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Graph Sig, Int) -> BDD a
forall a. HasCallStack => (Graph Sig, Int) -> BDD a
fromGraph (Graph Sig, 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 (Leaf Bool
b) = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> BDD a
forall a. Bool -> BDD a
Leaf (Bool -> Bool
not Bool
b))
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 (Leaf Bool
b1) (Leaf Bool
b2) = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just (Bool -> BDD a
forall a. Bool -> BDD a
Leaf (Bool
b1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b2))
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 (Leaf Bool
b) BDD a
t BDD a
e = if Bool
b then BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
t else 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
pbAtLeast :: forall a w. (ItemOrder a, Real w) => IntMap w -> w -> BDD a
pbAtLeast :: IntMap w -> w -> BDD a
pbAtLeast IntMap w
xs w
k0 = ((Int, w) -> Sig (Int, w)) -> (Int, w) -> BDD a
forall a b. (ItemOrder a, Ord b) => (b -> Sig b) -> b -> BDD a
unfoldOrd (Int, w) -> Sig (Int, w)
f (Int
0, w
k0)
where
xs' :: V.Vector (Int, w)
xs' :: Vector (Int, w)
xs' = [(Int, w)] -> Vector (Int, w)
forall a. [a] -> Vector a
V.fromList ([(Int, w)] -> Vector (Int, w)) -> [(Int, w)] -> Vector (Int, w)
forall a b. (a -> b) -> a -> b
$ ((Int, w) -> (Int, w) -> Ordering) -> [(Int, w)] -> [(Int, w)]
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, w) -> Int) -> (Int, w) -> (Int, w) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, w) -> Int
forall a b. (a, b) -> a
fst) ([(Int, w)] -> [(Int, w)]) -> [(Int, w)] -> [(Int, w)]
forall a b. (a -> b) -> a -> b
$ IntMap w -> [(Int, w)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap w
xs
ys :: V.Vector (w, w)
ys :: Vector (w, w)
ys = ((Int, w) -> (w, w) -> (w, w))
-> (w, w) -> Vector (Int, w) -> Vector (w, w)
forall a b. (a -> b -> b) -> b -> Vector a -> Vector b
V.scanr (\(Int
_, w
w) (w
lb,w
ub) -> if w
w w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
0 then (w
lb, w
ubw -> w -> w
forall a. Num a => a -> a -> a
+w
w) else (w
lbw -> w -> w
forall a. Num a => a -> a -> a
+w
w, w
ub)) (w
0,w
0) Vector (Int, w)
xs'
f :: (Int, w) -> Sig (Int, w)
f :: (Int, w) -> Sig (Int, w)
f (!Int
i, !w
k)
| Bool -> Bool
not (w
k w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
ub) = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
False
| Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector (Int, w) -> Int
forall a. Vector a -> Int
V.length Vector (Int, w)
xs' Bool -> Bool -> Bool
&& w
0 w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
k = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
True
| w
lb w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
k = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
True
| Bool
otherwise = Int -> (Int, w) -> (Int, w) -> Sig (Int, w)
forall a. Int -> a -> a -> Sig a
SBranch Int
x (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
k) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
kw -> w -> w
forall a. Num a => a -> a -> a
-w
w)
where
(w
lb,w
ub) = Vector (w, w)
ys Vector (w, w) -> Int -> (w, w)
forall a. Vector a -> Int -> a
V.! Int
i
(Int
x, w
w) = Vector (Int, w)
xs' Vector (Int, w) -> Int -> (Int, w)
forall a. Vector a -> Int -> a
V.! Int
i
pbAtMost :: forall a w. (ItemOrder a, Real w) => IntMap w -> w -> BDD a
pbAtMost :: IntMap w -> w -> BDD a
pbAtMost IntMap w
xs w
k0 = ((Int, w) -> Sig (Int, w)) -> (Int, w) -> BDD a
forall a b. (ItemOrder a, Ord b) => (b -> Sig b) -> b -> BDD a
unfoldOrd (Int, w) -> Sig (Int, w)
f (Int
0, w
k0)
where
xs' :: V.Vector (Int, w)
xs' :: Vector (Int, w)
xs' = [(Int, w)] -> Vector (Int, w)
forall a. [a] -> Vector a
V.fromList ([(Int, w)] -> Vector (Int, w)) -> [(Int, w)] -> Vector (Int, w)
forall a b. (a -> b) -> a -> b
$ ((Int, w) -> (Int, w) -> Ordering) -> [(Int, w)] -> [(Int, w)]
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, w) -> Int) -> (Int, w) -> (Int, w) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, w) -> Int
forall a b. (a, b) -> a
fst) ([(Int, w)] -> [(Int, w)]) -> [(Int, w)] -> [(Int, w)]
forall a b. (a -> b) -> a -> b
$ IntMap w -> [(Int, w)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap w
xs
ys :: V.Vector (w, w)
ys :: Vector (w, w)
ys = ((Int, w) -> (w, w) -> (w, w))
-> (w, w) -> Vector (Int, w) -> Vector (w, w)
forall a b. (a -> b -> b) -> b -> Vector a -> Vector b
V.scanr (\(Int
_, w
w) (w
lb,w
ub) -> if w
w w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
0 then (w
lb, w
ubw -> w -> w
forall a. Num a => a -> a -> a
+w
w) else (w
lbw -> w -> w
forall a. Num a => a -> a -> a
+w
w, w
ub)) (w
0,w
0) Vector (Int, w)
xs'
f :: (Int, w) -> Sig (Int, w)
f :: (Int, w) -> Sig (Int, w)
f (!Int
i, !w
k)
| Bool -> Bool
not (w
lb w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
k) = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
False
| Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector (Int, w) -> Int
forall a. Vector a -> Int
V.length Vector (Int, w)
xs' Bool -> Bool -> Bool
&& w
0 w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
k = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
True
| w
ub w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
k = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
True
| Bool
otherwise = Int -> (Int, w) -> (Int, w) -> Sig (Int, w)
forall a. Int -> a -> a -> Sig a
SBranch Int
x (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
k) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
kw -> w -> w
forall a. Num a => a -> a -> a
-w
w)
where
(w
lb,w
ub) = Vector (w, w)
ys Vector (w, w) -> Int -> (w, w)
forall a. Vector a -> Int -> a
V.! Int
i
(Int
x, w
w) = Vector (Int, w)
xs' Vector (Int, w) -> Int -> (Int, w)
forall a. Vector a -> Int -> a
V.! Int
i
pbExactly :: forall a w. (ItemOrder a, Real w) => IntMap w -> w -> BDD a
pbExactly :: IntMap w -> w -> BDD a
pbExactly IntMap w
xs w
k0 = ((Int, w) -> Sig (Int, w)) -> (Int, w) -> BDD a
forall a b. (ItemOrder a, Ord b) => (b -> Sig b) -> b -> BDD a
unfoldOrd (Int, w) -> Sig (Int, w)
f (Int
0, w
k0)
where
xs' :: V.Vector (Int, w)
xs' :: Vector (Int, w)
xs' = [(Int, w)] -> Vector (Int, w)
forall a. [a] -> Vector a
V.fromList ([(Int, w)] -> Vector (Int, w)) -> [(Int, w)] -> Vector (Int, w)
forall a b. (a -> b) -> a -> b
$ ((Int, w) -> (Int, w) -> Ordering) -> [(Int, w)] -> [(Int, w)]
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, w) -> Int) -> (Int, w) -> (Int, w) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, w) -> Int
forall a b. (a, b) -> a
fst) ([(Int, w)] -> [(Int, w)]) -> [(Int, w)] -> [(Int, w)]
forall a b. (a -> b) -> a -> b
$ IntMap w -> [(Int, w)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap w
xs
ys :: V.Vector (w, w)
ys :: Vector (w, w)
ys = ((Int, w) -> (w, w) -> (w, w))
-> (w, w) -> Vector (Int, w) -> Vector (w, w)
forall a b. (a -> b -> b) -> b -> Vector a -> Vector b
V.scanr (\(Int
_, w
w) (w
lb,w
ub) -> if w
w w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
0 then (w
lb, w
ubw -> w -> w
forall a. Num a => a -> a -> a
+w
w) else (w
lbw -> w -> w
forall a. Num a => a -> a -> a
+w
w, w
ub)) (w
0,w
0) Vector (Int, w)
xs'
f :: (Int, w) -> Sig (Int, w)
f :: (Int, w) -> Sig (Int, w)
f (!Int
i, !w
k)
| Bool -> Bool
not (w
lb w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
k Bool -> Bool -> Bool
&& w
k w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
ub) = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
False
| Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector (Int, w) -> Int
forall a. Vector a -> Int
V.length Vector (Int, w)
xs' Bool -> Bool -> Bool
&& w
0 w -> w -> Bool
forall a. Eq a => a -> a -> Bool
== w
k = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
True
| Bool
otherwise = Int -> (Int, w) -> (Int, w) -> Sig (Int, w)
forall a. Int -> a -> a -> Sig a
SBranch Int
x (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
k) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
kw -> w -> w
forall a. Num a => a -> a -> a
-w
w)
where
(w
lb,w
ub) = Vector (w, w)
ys Vector (w, w) -> Int -> (w, w)
forall a. Vector a -> Int -> a
V.! Int
i
(Int
x, w
w) = Vector (Int, w)
xs' Vector (Int, w) -> Int -> (Int, w)
forall a. Vector a -> Int -> a
V.! Int
i
pbExactlyIntegral :: forall a w. (ItemOrder a, Real w, Integral w) => IntMap w -> w -> BDD a
pbExactlyIntegral :: IntMap w -> w -> BDD a
pbExactlyIntegral IntMap w
xs w
k0 = ((Int, w) -> Sig (Int, w)) -> (Int, w) -> BDD a
forall a b. (ItemOrder a, Ord b) => (b -> Sig b) -> b -> BDD a
unfoldOrd (Int, w) -> Sig (Int, w)
f (Int
0, w
k0)
where
xs' :: V.Vector (Int, w)
xs' :: Vector (Int, w)
xs' = [(Int, w)] -> Vector (Int, w)
forall a. [a] -> Vector a
V.fromList ([(Int, w)] -> Vector (Int, w)) -> [(Int, w)] -> Vector (Int, w)
forall a b. (a -> b) -> a -> b
$ ((Int, w) -> (Int, w) -> Ordering) -> [(Int, w)] -> [(Int, w)]
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, w) -> Int) -> (Int, w) -> (Int, w) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, w) -> Int
forall a b. (a, b) -> a
fst) ([(Int, w)] -> [(Int, w)]) -> [(Int, w)] -> [(Int, w)]
forall a b. (a -> b) -> a -> b
$ IntMap w -> [(Int, w)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap w
xs
ys :: V.Vector (w, w)
ys :: Vector (w, w)
ys = ((Int, w) -> (w, w) -> (w, w))
-> (w, w) -> Vector (Int, w) -> Vector (w, w)
forall a b. (a -> b -> b) -> b -> Vector a -> Vector b
V.scanr (\(Int
_, w
w) (w
lb,w
ub) -> if w
w w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
0 then (w
lb, w
ubw -> w -> w
forall a. Num a => a -> a -> a
+w
w) else (w
lbw -> w -> w
forall a. Num a => a -> a -> a
+w
w, w
ub)) (w
0,w
0) Vector (Int, w)
xs'
ds :: V.Vector w
ds :: Vector w
ds = (w -> w -> w) -> Vector w -> Vector w
forall a. (a -> a -> a) -> Vector a -> Vector a
V.scanr1 (\w
w w
d -> if w
w w -> w -> Bool
forall a. Eq a => a -> a -> Bool
/= w
0 then w -> w -> w
forall a. Integral a => a -> a -> a
gcd w
w w
d else w
d) (((Int, w) -> w) -> Vector (Int, w) -> Vector w
forall a b. (a -> b) -> Vector a -> Vector b
V.map (Int, w) -> w
forall a b. (a, b) -> b
snd Vector (Int, w)
xs')
f :: (Int, w) -> Sig (Int, w)
f :: (Int, w) -> Sig (Int, w)
f (!Int
i, !w
k)
| Bool -> Bool
not (w
lb w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
k Bool -> Bool -> Bool
&& w
k w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
ub) = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
False
| Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector (Int, w) -> Int
forall a. Vector a -> Int
V.length Vector (Int, w)
xs' Bool -> Bool -> Bool
&& w
0 w -> w -> Bool
forall a. Eq a => a -> a -> Bool
== w
k = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
True
| w
d w -> w -> Bool
forall a. Eq a => a -> a -> Bool
/= w
0 Bool -> Bool -> Bool
&& w
k w -> w -> w
forall a. Integral a => a -> a -> a
`mod` w
d w -> w -> Bool
forall a. Eq a => a -> a -> Bool
/= w
0 = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
False
| Bool
otherwise = Int -> (Int, w) -> (Int, w) -> Sig (Int, w)
forall a. Int -> a -> a -> Sig a
SBranch Int
x (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
k) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
kw -> w -> w
forall a. Num a => a -> a -> a
-w
w)
where
(w
lb,w
ub) = Vector (w, w)
ys Vector (w, w) -> Int -> (w, w)
forall a. Vector a -> Int -> a
V.! Int
i
(Int
x, w
w) = Vector (Int, w)
xs' Vector (Int, w) -> Int -> (Int, w)
forall a. Vector a -> Int -> a
V.! Int
i
d :: w
d = Vector w
ds Vector w -> Int -> w
forall a. Vector a -> Int -> a
V.! Int
i
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 :: (Int -> b -> b -> b) -> (Bool -> b) -> BDD a -> b
fold :: (Int -> b -> b -> b) -> (Bool -> b) -> BDD a -> b
fold Int -> b -> b -> b
br Bool -> b
lf (BDD Node
node) = (Int -> b -> b -> b) -> (Bool -> b) -> Node -> b
forall a. (Int -> a -> a -> a) -> (Bool -> a) -> Node -> a
Node.fold Int -> b -> b -> b
br Bool -> b
lf Node
node
fold' :: (Int -> b -> b -> b) -> (Bool -> b) -> BDD a -> b
fold' :: (Int -> b -> b -> b) -> (Bool -> b) -> BDD a -> b
fold' Int -> b -> b -> b
br Bool -> b
lf (BDD Node
node) = (Int -> b -> b -> b) -> (Bool -> b) -> Node -> b
forall a. (Int -> a -> a -> a) -> (Bool -> a) -> Node -> a
Node.fold' Int -> b -> b -> b
br Bool -> b
lf Node
node
mkFold'Op :: (Int -> b -> b -> b) -> (Bool -> b) -> ST s (BDD a -> ST s b)
mkFold'Op :: (Int -> b -> b -> b) -> (Bool -> b) -> ST s (BDD a -> ST s b)
mkFold'Op Int -> b -> b -> b
br Bool -> b
lf = do
Node -> ST s b
op <- (Int -> b -> b -> b) -> (Bool -> b) -> ST s (Node -> ST s b)
forall a s.
(Int -> a -> a -> a) -> (Bool -> a) -> ST s (Node -> ST s a)
Node.mkFold'Op Int -> b -> b -> b
br Bool -> b
lf
(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) -> ST s (BDD a -> ST s b))
-> (BDD a -> ST s b) -> ST s (BDD a -> ST s b)
forall a b. (a -> b) -> a -> b
$ \(BDD Node
node) -> Node -> ST s b
op Node
node
unfoldHashable :: forall a b. (ItemOrder a, Eq b, Hashable b) => (b -> Sig b) -> b -> BDD a
unfoldHashable :: (b -> Sig b) -> b -> BDD a
unfoldHashable b -> Sig b
f b
b = (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 b (Sig b)
h <- Int -> ST s (HashTable s b (Sig b))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
let g :: [b] -> ST s ()
g [] = () -> ST s ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
g (b
x : [b]
xs) = do
Maybe (Sig b)
r <- HashTable s b (Sig b) -> b -> ST s (Maybe (Sig 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 b (Sig b)
h b
x
case Maybe (Sig b)
r of
Just Sig b
_ -> [b] -> ST s ()
g [b]
xs
Maybe (Sig b)
Nothing -> do
let fx :: Sig b
fx = b -> Sig b
f b
x
HashTable s b (Sig b) -> b -> Sig 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 b (Sig b)
h b
x Sig b
fx
[b] -> ST s ()
g ([b]
xs [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ Sig b -> [b]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList Sig b
fx)
[b] -> ST s ()
g [b
b]
[(b, Sig b)]
xs <- HashTable s b (Sig b) -> ST s [(b, Sig b)]
forall (h :: * -> * -> * -> *) s k v.
HashTable h =>
h s k v -> ST s [(k, v)]
H.toList HashTable s b (Sig b)
h
let h2 :: HashMap b (BDD a)
h2 = [(b, BDD a)] -> HashMap b (BDD a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList [(b
x, Sig (BDD a) -> BDD a
forall a. Sig (BDD a) -> BDD a
inSig ((b -> BDD a) -> Sig b -> Sig (BDD a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HashMap b (BDD a)
h2 HashMap b (BDD a) -> b -> BDD a
forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
HashMap.!) Sig b
s)) | (b
x,Sig b
s) <- [(b, Sig b)]
xs]
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
$ HashMap b (BDD a)
forall a. HashMap b (BDD a)
h2 HashMap b (BDD a) -> b -> BDD a
forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
HashMap.! b
b
unfoldOrd :: forall a b. (ItemOrder a, Ord b) => (b -> Sig b) -> b -> BDD a
unfoldOrd :: (b -> Sig b) -> b -> BDD a
unfoldOrd b -> Sig b
f b
b = Map b (BDD a)
m2 Map b (BDD a) -> b -> BDD a
forall k a. Ord k => Map k a -> k -> a
Map.! b
b
where
m1 :: Map b (Sig b)
m1 :: Map b (Sig b)
m1 = Map b (Sig b) -> [b] -> Map b (Sig b)
g Map b (Sig b)
forall k a. Map k a
Map.empty [b
b]
m2 :: Map b (BDD a)
m2 :: Map b (BDD a)
m2 = (Sig b -> BDD a) -> Map b (Sig b) -> Map b (BDD a)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Sig (BDD a) -> BDD a
forall a. Sig (BDD a) -> BDD a
inSig (Sig (BDD a) -> BDD a) -> (Sig b -> Sig (BDD a)) -> Sig b -> BDD a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> BDD a) -> Sig b -> Sig (BDD a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Map b (BDD a)
m2 Map b (BDD a) -> b -> BDD a
forall k a. Ord k => Map k a -> k -> a
Map.!)) Map b (Sig b)
m1
g :: Map b (Sig b) -> [b] -> Map b (Sig b)
g Map b (Sig b)
m [] = Map b (Sig b)
m
g Map b (Sig b)
m (b
x : [b]
xs) =
case b -> Map b (Sig b) -> Maybe (Sig b)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup b
x Map b (Sig b)
m of
Just Sig b
_ -> Map b (Sig b) -> [b] -> Map b (Sig b)
g Map b (Sig b)
m [b]
xs
Maybe (Sig b)
Nothing ->
let fx :: Sig b
fx = b -> Sig b
f b
x
in Map b (Sig b) -> [b] -> Map b (Sig b)
g (b -> Sig b -> Map b (Sig b) -> Map b (Sig b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert b
x Sig b
fx Map b (Sig b)
m) ([b]
xs [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ Sig b -> [b]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList Sig b
fx)
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 = (Int -> IntSet -> IntSet -> IntSet)
-> (Bool -> IntSet) -> ST s (BDD a -> ST s IntSet)
forall b s a.
(Int -> b -> b -> b) -> (Bool -> b) -> ST s (BDD a -> ST s b)
mkFold'Op Int -> IntSet -> IntSet -> IntSet
f Bool -> IntSet
forall p. p -> IntSet
g
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)
g :: p -> IntSet
g p
_ = IntSet
IntSet.empty
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 (Leaf Bool
b) = Bool
b
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
numNodes :: BDD a -> Int
numNodes :: BDD a -> Int
numNodes (BDD Node
node) = Node -> Int
Node.numNodes Node
node
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 n :: BDD a
n@(Leaf Bool
_) = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
n
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)]
_ n :: BDD a
n@(Leaf Bool
_) = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
n
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
_ n :: BDD a
n@(Leaf Bool
_) = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
n
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 (Leaf Bool
b) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b
asBool BDD a
_ = Maybe Bool
forall a. Maybe a
Nothing
lfp :: ItemOrder a => (BDD a -> BDD a) -> BDD a
lfp :: (BDD a -> BDD a) -> BDD a
lfp BDD a -> BDD a
f = BDD a -> BDD a
go BDD a
forall a. BDD a
false
where
go :: BDD a -> BDD a
go BDD a
curr
| BDD a
curr BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
next = BDD a
curr
| Bool
otherwise = BDD a -> BDD a
go BDD a
next
where
next :: BDD a
next = BDD a -> BDD a
f BDD a
curr
gfp :: ItemOrder a => (BDD a -> BDD a) -> BDD a
gfp :: (BDD a -> BDD a) -> BDD a
gfp BDD a -> BDD a
f = BDD a -> BDD a
go BDD a
forall a. BDD a
true
where
go :: BDD a -> BDD a
go BDD a
curr
| BDD a
curr BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
next = BDD a
curr
| Bool
otherwise = BDD a -> BDD a
go BDD a
next
where
next :: BDD a
next = BDD a -> BDD a
f BDD a
curr
findSatM :: MonadPlus m => BDD a -> m (IntMap Bool)
findSatM :: BDD a -> m (IntMap Bool)
findSatM = (Int -> m (IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool))
-> (Bool -> m (IntMap Bool)) -> BDD a -> m (IntMap Bool)
forall b a. (Int -> b -> b -> b) -> (Bool -> b) -> BDD a -> b
fold Int -> m (IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *).
MonadPlus m =>
Int -> m (IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
f Bool -> m (IntMap Bool)
forall (m :: * -> *) a. MonadPlus m => Bool -> m (IntMap a)
g
where
f :: Int -> m (IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
f Int
x m (IntMap Bool)
lo m (IntMap Bool)
hi = m (IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus ((IntMap Bool -> IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
False) m (IntMap Bool)
lo) ((IntMap Bool -> IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
True) m (IntMap Bool)
hi)
g :: Bool -> m (IntMap a)
g Bool
b = if Bool
b then IntMap a -> m (IntMap a)
forall (m :: * -> *) a. Monad m => a -> m a
return IntMap a
forall a. IntMap a
IntMap.empty else m (IntMap a)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
anySat :: BDD a -> Maybe (IntMap Bool)
anySat :: BDD a -> Maybe (IntMap Bool)
anySat = BDD a -> Maybe (IntMap Bool)
forall (m :: * -> *) a. MonadPlus m => BDD a -> m (IntMap Bool)
findSatM
allSat :: BDD a -> [IntMap Bool]
allSat :: BDD a -> [IntMap Bool]
allSat = BDD a -> [IntMap Bool]
forall (m :: * -> *) a. MonadPlus m => BDD a -> m (IntMap Bool)
findSatM
findSatCompleteM :: forall a m. (MonadPlus m, ItemOrder a, HasCallStack) => IntSet -> BDD a -> m (IntMap Bool)
findSatCompleteM :: IntSet -> BDD a -> m (IntMap Bool)
findSatCompleteM IntSet
xs0 BDD a
bdd = (forall s. ST s (m (IntMap Bool))) -> m (IntMap Bool)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (m (IntMap Bool))) -> m (IntMap Bool))
-> (forall s. ST s (m (IntMap Bool))) -> m (IntMap Bool)
forall a b. (a -> b) -> a -> b
$ do
HashTable s (BDD a) (m (IntMap Bool))
h <- Int -> ST s (HashTable s (BDD a) (m (IntMap Bool)))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
let f :: [Int] -> BDD a -> ST s (m (IntMap Bool))
f [Int]
_ (Leaf Bool
False) = m (IntMap Bool) -> ST s (m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (m (IntMap Bool) -> ST s (m (IntMap Bool)))
-> m (IntMap Bool) -> ST s (m (IntMap Bool))
forall a b. (a -> b) -> a -> b
$ m (IntMap Bool)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
f [Int]
xs (Leaf Bool
True) = m (IntMap Bool) -> ST s (m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (m (IntMap Bool) -> ST s (m (IntMap Bool)))
-> m (IntMap Bool) -> ST s (m (IntMap Bool))
forall a b. (a -> b) -> a -> b
$ (IntMap Bool -> Int -> m (IntMap Bool))
-> IntMap Bool -> [Int] -> m (IntMap Bool)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\IntMap Bool
m Int
x -> [m (IntMap Bool)] -> m (IntMap Bool)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [IntMap Bool -> m (IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
v IntMap Bool
m) | Bool
v <- [Bool
False, Bool
True]]) IntMap Bool
forall a. IntMap a
IntMap.empty [Int]
xs
f [Int]
xs n :: BDD a
n@(Branch Int
x BDD a
lo BDD a
hi) = do
case (Int -> Bool) -> [Int] -> ([Int], [Int])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\Int
x2 -> 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
x2 Int
x Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT) [Int]
xs of
([Int]
ys, (Int
x':[Int]
xs')) | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' -> do
Maybe (m (IntMap Bool))
r <- HashTable s (BDD a) (m (IntMap Bool))
-> BDD a -> ST s (Maybe (m (IntMap Bool)))
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) (m (IntMap Bool))
h BDD a
n
m (IntMap Bool)
ps <- case Maybe (m (IntMap Bool))
r of
Just m (IntMap Bool)
ret -> m (IntMap Bool) -> ST s (m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return m (IntMap Bool)
ret
Maybe (m (IntMap Bool))
Nothing -> do
m (IntMap Bool)
r0 <- [Int] -> BDD a -> ST s (m (IntMap Bool))
f [Int]
xs' BDD a
lo
m (IntMap Bool)
r1 <- ST s (m (IntMap Bool)) -> ST s (m (IntMap Bool))
forall s a. ST s a -> ST s a
unsafeInterleaveST (ST s (m (IntMap Bool)) -> ST s (m (IntMap Bool)))
-> ST s (m (IntMap Bool)) -> ST s (m (IntMap Bool))
forall a b. (a -> b) -> a -> b
$ [Int] -> BDD a -> ST s (m (IntMap Bool))
f [Int]
xs' BDD a
hi
let ret :: m (IntMap Bool)
ret = (IntMap Bool -> IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
False) m (IntMap Bool)
r0 m (IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` (IntMap Bool -> IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
True) m (IntMap Bool)
r1
HashTable s (BDD a) (m (IntMap Bool))
-> BDD a -> m (IntMap Bool) -> 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) (m (IntMap Bool))
h BDD a
n m (IntMap Bool)
ret
m (IntMap Bool) -> ST s (m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return m (IntMap Bool)
ret
m (IntMap Bool) -> ST s (m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (m (IntMap Bool) -> ST s (m (IntMap Bool)))
-> m (IntMap Bool) -> ST s (m (IntMap Bool))
forall a b. (a -> b) -> a -> b
$ do
IntMap Bool
p <- m (IntMap Bool)
ps
(IntMap Bool -> Int -> m (IntMap Bool))
-> IntMap Bool -> [Int] -> m (IntMap Bool)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\IntMap Bool
m Int
y -> [m (IntMap Bool)] -> m (IntMap Bool)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [IntMap Bool -> m (IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
y Bool
v IntMap Bool
m) | Bool
v <- [Bool
False, Bool
True]]) IntMap Bool
p [Int]
ys
([Int], [Int])
_ -> String -> ST s (m (IntMap Bool))
forall a. HasCallStack => String -> a
error (String
"findSatCompleteM: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" should not occur")
[Int] -> BDD a -> ST s (m (IntMap Bool))
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
xs0)) BDD a
bdd
anySatComplete :: ItemOrder a => IntSet -> BDD a -> Maybe (IntMap Bool)
anySatComplete :: IntSet -> BDD a -> Maybe (IntMap Bool)
anySatComplete = IntSet -> BDD a -> Maybe (IntMap Bool)
forall a (m :: * -> *).
(MonadPlus m, ItemOrder a, HasCallStack) =>
IntSet -> BDD a -> m (IntMap Bool)
findSatCompleteM
allSatComplete :: ItemOrder a => IntSet -> BDD a -> [IntMap Bool]
allSatComplete :: IntSet -> BDD a -> [IntMap Bool]
allSatComplete = IntSet -> BDD a -> [IntMap Bool]
forall a (m :: * -> *).
(MonadPlus m, ItemOrder a, HasCallStack) =>
IntSet -> BDD a -> m (IntMap Bool)
findSatCompleteM
{-# SPECIALIZE countSat :: ItemOrder a => IntSet -> BDD a -> Int #-}
{-# SPECIALIZE countSat :: ItemOrder a => IntSet -> BDD a -> Integer #-}
{-# SPECIALIZE countSat :: ItemOrder a => IntSet -> BDD a -> Natural #-}
countSat :: forall a b. (ItemOrder a, Num b, Bits b, HasCallStack) => IntSet -> BDD a -> b
countSat :: IntSet -> BDD a -> b
countSat IntSet
xs 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 :: [Int] -> BDD a -> ST s b
f [Int]
_ (Leaf Bool
False) = b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> ST s b) -> b -> ST s b
forall a b. (a -> b) -> a -> b
$ b
0
f [Int]
ys (Leaf Bool
True) = b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> ST s b) -> b -> ST s b
forall a b. (a -> b) -> a -> b
$! b
1 b -> Int -> b
forall a. Bits a => a -> Int -> a
`shiftL` [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
ys
f [Int]
ys node :: BDD a
node@(Branch Int
x BDD a
lo BDD a
hi) = do
case (Int -> Bool) -> [Int] -> ([Int], [Int])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\Int
x2 -> 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
x2 Int
x Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT) [Int]
ys of
([Int]
zs, Int
y' : [Int]
ys') | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y' -> 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
node
b
n <- case Maybe b
m of
Just b
n -> b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
n
Maybe b
Nothing -> do
b
n <- (b -> b -> b) -> ST s b -> ST s b -> ST s b
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 b -> b -> b
forall a. Num a => a -> a -> a
(+) ([Int] -> BDD a -> ST s b
f [Int]
ys' BDD a
lo) ([Int] -> BDD a -> ST s b
f [Int]
ys' BDD a
hi)
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
node b
n
b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
n
b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> ST s b) -> b -> ST s b
forall a b. (a -> b) -> a -> b
$! b
n b -> Int -> b
forall a. Bits a => a -> Int -> a
`shiftL` [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
zs
([Int]
_, [Int]
_) -> String -> ST s b
forall a. HasCallStack => String -> a
error (String
"countSat: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" should not occur")
[Int] -> BDD a -> ST s b
f ((Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) (IntSet -> [Int]
IntSet.toList IntSet
xs)) BDD a
bdd
#if MIN_VERSION_mwc_random(0,15,0)
uniformSatM :: forall a g m. (ItemOrder a, StatefulGen g m, HasCallStack) => IntSet -> BDD a -> g -> m (IntMap Bool)
#else
uniformSatM :: forall a m. (ItemOrder a, PrimMonad m, HasCallStack) => IntSet -> BDD a -> Gen (PrimState m) -> m (IntMap Bool)
#endif
uniformSatM :: IntSet -> BDD a -> g -> m (IntMap Bool)
uniformSatM IntSet
xs0 BDD a
bdd0 = IntMap Bool -> g -> m (IntMap Bool)
func IntMap Bool
forall a. IntMap a
IntMap.empty
where
func :: IntMap Bool -> g -> m (IntMap Bool)
func = (forall s. ST s (IntMap Bool -> g -> m (IntMap Bool)))
-> IntMap Bool -> g -> m (IntMap Bool)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (IntMap Bool -> g -> m (IntMap Bool)))
-> IntMap Bool -> g -> m (IntMap Bool))
-> (forall s. ST s (IntMap Bool -> g -> m (IntMap Bool)))
-> IntMap Bool
-> g
-> m (IntMap Bool)
forall a b. (a -> b) -> a -> b
$ do
HashTable s (BDD a) (Integer, IntMap Bool -> g -> m (IntMap Bool))
h <- Int
-> ST
s
(HashTable
s (BDD a) (Integer, IntMap Bool -> g -> m (IntMap Bool)))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
let f :: [Int]
-> BDD a -> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
f [Int]
xs BDD a
bdd =
case (Int -> Bool) -> [Int] -> ([Int], [Int])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\Int
x2 -> Int -> Level a
forall a. Int -> Level a
NonTerminal Int
x2 Level a -> Level a -> Bool
forall a. Ord a => a -> a -> Bool
< BDD a -> Level a
forall a. BDD a -> Level a
level BDD a
bdd) [Int]
xs of
([Int]
ys, [Int]
xxs') -> do
[Int]
xs' <- case (BDD a
bdd, [Int]
xxs') of
(Branch Int
x BDD a
_ BDD a
_, Int
x' : [Int]
xs') | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' -> [Int] -> ST s [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return [Int]
xs'
(Branch Int
x BDD a
_ BDD a
_, [Int]
_) -> String -> ST s [Int]
forall a. HasCallStack => String -> a
error (String
"uniformSatM: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" should not occur")
(Leaf Bool
_, []) -> [Int] -> ST s [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return []
(Leaf Bool
_, Int
_:[Int]
_) -> String -> ST s [Int]
forall a. HasCallStack => String -> a
error (String
"uniformSatM: should not happen")
(Integer
s, IntMap Bool -> g -> m (IntMap Bool)
func0) <- [Int]
-> BDD a -> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
g [Int]
xs' BDD a
bdd
let func' :: IntMap Bool -> g -> m (IntMap Bool)
func' !IntMap Bool
m !g
gen = do
#if MIN_VERSION_mwc_random(0,15,0)
[Bool]
vals <- Int -> m Bool -> m [Bool]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM ([Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
ys) (g -> m Bool
forall a g (m :: * -> *). (Uniform a, StatefulGen g m) => g -> m a
uniformM g
gen)
#else
vals <- replicateM (length ys) (uniform gen)
#endif
IntMap Bool -> g -> m (IntMap Bool)
func0 (IntMap Bool
m IntMap Bool -> IntMap Bool -> IntMap Bool
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` [(Int, Bool)] -> IntMap Bool
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
ys [Bool]
vals)) g
gen
(Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
s Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
ys, IntMap Bool -> g -> m (IntMap Bool)
func')
g :: [Int]
-> BDD a -> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
g [Int]
_ (Leaf Bool
True) = (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
1 :: Integer, \IntMap Bool
a g
_gen -> IntMap Bool -> m (IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return IntMap Bool
a)
g [Int]
_ (Leaf Bool
False) = (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
0 :: Integer, \IntMap Bool
_a g
_gen -> String -> m (IntMap Bool)
forall a. HasCallStack => String -> a
error String
"uniformSatM: should not happen")
g [Int]
xs bdd :: BDD a
bdd@(Branch Int
x BDD a
lo BDD a
hi) = do
Maybe (Integer, IntMap Bool -> g -> m (IntMap Bool))
m <- HashTable s (BDD a) (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> BDD a
-> ST s (Maybe (Integer, IntMap Bool -> g -> m (IntMap Bool)))
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) (Integer, IntMap Bool -> g -> m (IntMap Bool))
h BDD a
bdd
case Maybe (Integer, IntMap Bool -> g -> m (IntMap Bool))
m of
Just (Integer, IntMap Bool -> g -> m (IntMap Bool))
ret -> (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer, IntMap Bool -> g -> m (IntMap Bool))
ret
Maybe (Integer, IntMap Bool -> g -> m (IntMap Bool))
Nothing -> do
(Integer
n0, IntMap Bool -> g -> m (IntMap Bool)
func0) <- [Int]
-> BDD a -> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
f [Int]
xs BDD a
lo
(Integer
n1, IntMap Bool -> g -> m (IntMap Bool)
func1) <- [Int]
-> BDD a -> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
f [Int]
xs BDD a
hi
let s :: Integer
s = Integer
n0 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n1
r :: Double
r :: Double
r = Ratio Integer -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Integer
n1 Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
s)
Double -> ST s () -> ST s ()
seq Double
r (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 ()
let func' :: IntMap Bool -> g -> m (IntMap Bool)
func' !IntMap Bool
a !g
gen = do
Bool
b <- Double -> g -> m Bool
forall g (m :: * -> *). StatefulGen g m => Double -> g -> m Bool
bernoulli Double
r g
gen
if Bool
b then
IntMap Bool -> g -> m (IntMap Bool)
func1 (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
True IntMap Bool
a) g
gen
else
IntMap Bool -> g -> m (IntMap Bool)
func0 (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
False IntMap Bool
a) g
gen
HashTable s (BDD a) (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> BDD a
-> (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> 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) (Integer, IntMap Bool -> g -> m (IntMap Bool))
h BDD a
bdd (Integer
s, IntMap Bool -> g -> m (IntMap Bool)
func')
(Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
s, IntMap Bool -> g -> m (IntMap Bool)
func')
((Integer, IntMap Bool -> g -> m (IntMap Bool))
-> IntMap Bool -> g -> m (IntMap Bool))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (IntMap Bool -> g -> m (IntMap Bool))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> IntMap Bool -> g -> m (IntMap Bool)
forall a b. (a, b) -> b
snd (ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (IntMap Bool -> g -> m (IntMap Bool)))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (IntMap Bool -> g -> m (IntMap Bool))
forall a b. (a -> b) -> a -> b
$ [Int]
-> BDD a -> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
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
xs0)) BDD a
bdd0
inSig :: Sig (BDD a) -> BDD a
inSig :: Sig (BDD a) -> BDD a
inSig (SLeaf Bool
b) = Bool -> BDD a
forall a. Bool -> BDD a
Leaf Bool
b
inSig (SBranch Int
x BDD a
lo 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
outSig :: BDD a -> Sig (BDD a)
outSig :: BDD a -> Sig (BDD a)
outSig (Leaf Bool
b) = Bool -> Sig (BDD a)
forall a. Bool -> Sig a
SLeaf Bool
b
outSig (Branch Int
x BDD a
lo BDD a
hi) = Int -> BDD a -> BDD a -> Sig (BDD a)
forall a. Int -> a -> a -> Sig a
SBranch Int
x BDD a
lo BDD a
hi
toGraph :: BDD a -> (Graph Sig, Int)
toGraph :: BDD a -> (Graph Sig, Int)
toGraph (BDD Node
node) = Node -> (Graph Sig, Int)
Node.toGraph Node
node
toGraph' :: Traversable t => t (BDD a) -> (Graph Sig, t Int)
toGraph' :: t (BDD a) -> (Graph Sig, t Int)
toGraph' t (BDD a)
bs = t Node -> (Graph Sig, t Int)
forall (t :: * -> *). Traversable t => t Node -> (Graph Sig, t Int)
Node.toGraph' ((BDD a -> Node) -> t (BDD a) -> t Node
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(BDD Node
node) -> Node
node) t (BDD a)
bs)
fromGraph :: HasCallStack => (Graph Sig, Int) -> BDD a
fromGraph :: (Graph Sig, Int) -> BDD a
fromGraph = (Sig (BDD a) -> BDD a) -> (Graph Sig, Int) -> BDD a
forall (f :: * -> *) a.
(Functor f, HasCallStack) =>
(f a -> a) -> (Graph f, Int) -> a
Node.foldGraph Sig (BDD a) -> BDD a
forall a. Sig (BDD a) -> BDD a
inSig
fromGraph' :: HasCallStack => Graph Sig -> IntMap (BDD a)
fromGraph' :: Graph Sig -> IntMap (BDD a)
fromGraph' = (Sig (BDD a) -> BDD a) -> Graph Sig -> IntMap (BDD a)
forall (f :: * -> *) a.
(Functor f, HasCallStack) =>
(f a -> a) -> Graph f -> IntMap a
Node.foldGraphNodes Sig (BDD a) -> BDD a
forall a. Sig (BDD a) -> BDD a
inSig