{-# language ScopedTypeVariables #-}
{-# language PatternGuards #-}
{-# language FlexibleContexts #-}

module OBDD.Operation 

( Boolean(..)
, equiv
, unary, binary
, instantiate
, exists, exists_many
, forall, forall_many
, fold, foldM
, full_fold, full_foldM
)

where

import OBDD.Data
import OBDD.Make
import Ersatz.Bit 
import Data.Foldable (toList)

import qualified Data.IntMap as IM
import qualified OBDD.IntIntMap as IIM
import qualified Data.Map as M

import qualified Control.Monad.State.Strict as T
import Control.Monad (forM_)
import qualified Data.List ( sortBy)
import Data.Function (on)

import Data.Set ( Set )
import qualified Data.Set as S

import Prelude hiding ( (&&), (||), and, or, not, any, all, bool )
import qualified Prelude
import qualified Data.Bool

instance Ord v => Boolean (OBDD v) where
  bool :: Bool -> OBDD v
bool Bool
f = Bool -> OBDD v
forall v. Ord v => Bool -> OBDD v
constant Bool
f
  not :: OBDD v -> OBDD v
not = OBDD v -> OBDD v
forall v. OBDD v -> OBDD v
not_
  ( && ) = (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
forall v.
Ord v =>
(Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
symmetric_binary ( Prelude.&& )
  ( || ) = (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
forall v.
Ord v =>
(Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
symmetric_binary ( Prelude.|| )
  choose :: OBDD v -> OBDD v -> OBDD v -> OBDD v
choose OBDD v
no OBDD v
yes OBDD v
sel =
    -- https://github.com/jwaldmann/haskell-obdd/issues/10
    (OBDD v
no OBDD v -> OBDD v -> OBDD v
forall b. Boolean b => b -> b -> b
&& OBDD v -> OBDD v
forall b. Boolean b => b -> b
not OBDD v
sel) OBDD v -> OBDD v -> OBDD v
forall b. Boolean b => b -> b -> b
|| (OBDD v
yes OBDD v -> OBDD v -> OBDD v
forall b. Boolean b => b -> b -> b
&& OBDD v
sel)
  xor :: OBDD v -> OBDD v -> OBDD v
xor   = (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
forall v.
Ord v =>
(Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
symmetric_binary Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)
  ( ==> ) = (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
forall v.
Ord v =>
(Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
binary ( <= )
  all :: (a -> OBDD v) -> t a -> OBDD v
all a -> OBDD v
p = OBDD v -> (OBDD v -> OBDD v -> OBDD v) -> [OBDD v] -> OBDD v
forall v.
OBDD v -> (OBDD v -> OBDD v -> OBDD v) -> [OBDD v] -> OBDD v
fold_by_size OBDD v
forall b. Boolean b => b
true  OBDD v -> OBDD v -> OBDD v
forall b. Boolean b => b -> b -> b
(&&) ([OBDD v] -> OBDD v) -> (t a -> [OBDD v]) -> t a -> OBDD v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> OBDD v) -> [a] -> [OBDD v]
forall a b. (a -> b) -> [a] -> [b]
map a -> OBDD v
p ([a] -> [OBDD v]) -> (t a -> [a]) -> t a -> [OBDD v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
  any :: (a -> OBDD v) -> t a -> OBDD v
any a -> OBDD v
p = OBDD v -> (OBDD v -> OBDD v -> OBDD v) -> [OBDD v] -> OBDD v
forall v.
OBDD v -> (OBDD v -> OBDD v -> OBDD v) -> [OBDD v] -> OBDD v
fold_by_size OBDD v
forall b. Boolean b => b
false OBDD v -> OBDD v -> OBDD v
forall b. Boolean b => b -> b -> b
(||) ([OBDD v] -> OBDD v) -> (t a -> [OBDD v]) -> t a -> OBDD v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> OBDD v) -> [a] -> [OBDD v]
forall a b. (a -> b) -> [a] -> [b]
map a -> OBDD v
p ([a] -> [OBDD v]) -> (t a -> [a]) -> t a -> [OBDD v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

equiv :: Ord v => OBDD v -> OBDD v -> OBDD v
equiv :: OBDD v -> OBDD v -> OBDD v
equiv = (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
forall v.
Ord v =>
(Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
symmetric_binary Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==)

fold_by_size :: OBDD v -> (OBDD v -> OBDD v -> OBDD v) -> [OBDD v] -> OBDD v
fold_by_size OBDD v
base OBDD v -> OBDD v -> OBDD v
reduce [OBDD v]
fs =
    let handle :: [OBDD v] -> OBDD v
handle [OBDD v]
fs = case [OBDD v]
fs of
            [] -> OBDD v
base
            [OBDD v
f1 ] -> OBDD v
f1
            OBDD v
f1 : OBDD v
f2 : [OBDD v]
rest -> 
                let f :: OBDD v
f = OBDD v -> OBDD v -> OBDD v
reduce OBDD v
f1 OBDD v
f2
                in  [OBDD v] -> OBDD v
handle ([OBDD v] -> OBDD v) -> [OBDD v] -> OBDD v
forall a b. (a -> b) -> a -> b
$ OBDD v -> [OBDD v] -> [OBDD v]
forall v. OBDD v -> [OBDD v] -> [OBDD v]
insert OBDD v
f [OBDD v]
rest
        insert :: OBDD v -> [OBDD v] -> [OBDD v]
insert OBDD v
f [OBDD v]
gs = case [OBDD v]
gs of
            OBDD v
g : [OBDD v]
hs | OBDD v -> Index
forall v. OBDD v -> Index
size OBDD v
f Index -> Index -> Bool
forall a. Ord a => a -> a -> Bool
> OBDD v -> Index
forall v. OBDD v -> Index
size OBDD v
g -> OBDD v
g OBDD v -> [OBDD v] -> [OBDD v]
forall a. a -> [a] -> [a]
: OBDD v -> [OBDD v] -> [OBDD v]
insert OBDD v
f [OBDD v]
hs
            [OBDD v]
_ -> OBDD v
f OBDD v -> [OBDD v] -> [OBDD v]
forall a. a -> [a] -> [a]
: [OBDD v]
gs
    in  [OBDD v] -> OBDD v
handle ([OBDD v] -> OBDD v) -> [OBDD v] -> OBDD v
forall a b. (a -> b) -> a -> b
$ (OBDD v -> OBDD v -> Ordering) -> [OBDD v] -> [OBDD v]
forall a. (a -> a -> Ordering) -> [a] -> [a]
Data.List.sortBy (Index -> Index -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Index -> Index -> Ordering)
-> (OBDD v -> Index) -> OBDD v -> OBDD v -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` OBDD v -> Index
forall v. OBDD v -> Index
size) [OBDD v]
fs


-- | FIXME: this function is nonsensical. There is only one interesting
-- unary Boolean function (negation), and it should be handled differently.
unary :: Ord v 
      => ( Bool -> Bool )
      -> OBDD v -> OBDD v
unary :: (Bool -> Bool) -> OBDD v -> OBDD v
unary Bool -> Bool
op OBDD v
x = State (OBDD v) Index -> OBDD v
forall v. State (OBDD v) Index -> OBDD v
make (State (OBDD v) Index -> OBDD v) -> State (OBDD v) Index -> OBDD v
forall a b. (a -> b) -> a -> b
$ do
    let handle :: OBDD v -> t (StateT (OBDD v) Identity) Index
handle OBDD v
x = Index
-> t (StateT (OBDD v) Identity) Index
-> t (StateT (OBDD v) Identity) Index
forall (m :: * -> *) b.
MonadState (IntMap b) m =>
Index -> m b -> m b
cachedIM (OBDD v -> Index
forall v. OBDD v -> Index
top OBDD v
x) (t (StateT (OBDD v) Identity) Index
 -> t (StateT (OBDD v) Identity) Index)
-> t (StateT (OBDD v) Identity) Index
-> t (StateT (OBDD v) Identity) Index
forall a b. (a -> b) -> a -> b
$ case OBDD v -> Node v (OBDD v)
forall v. OBDD v -> Node v (OBDD v)
access OBDD v
x of
                Leaf Bool
p -> do
                  StateT (OBDD v) Identity Index
-> t (StateT (OBDD v) Identity) Index
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
T.lift (StateT (OBDD v) Identity Index
 -> t (StateT (OBDD v) Identity) Index)
-> StateT (OBDD v) Identity Index
-> t (StateT (OBDD v) Identity) Index
forall a b. (a -> b) -> a -> b
$ Node v Index -> StateT (OBDD v) Identity Index
forall v. Ord v => Node v Index -> State (OBDD v) Index
register (Node v Index -> StateT (OBDD v) Identity Index)
-> Node v Index -> StateT (OBDD v) Identity Index
forall a b. (a -> b) -> a -> b
$ Bool -> Node v Index
forall v i. Bool -> Node v i
Leaf (Bool -> Node v Index) -> Bool -> Node v Index
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
op Bool
p
                Branch v
v OBDD v
l OBDD v
r -> do
                        Index
l' <- OBDD v -> t (StateT (OBDD v) Identity) Index
handle OBDD v
l
                        Index
r' <- OBDD v -> t (StateT (OBDD v) Identity) Index
handle OBDD v
r
                        StateT (OBDD v) Identity Index
-> t (StateT (OBDD v) Identity) Index
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
T.lift (StateT (OBDD v) Identity Index
 -> t (StateT (OBDD v) Identity) Index)
-> StateT (OBDD v) Identity Index
-> t (StateT (OBDD v) Identity) Index
forall a b. (a -> b) -> a -> b
$ Node v Index -> StateT (OBDD v) Identity Index
forall v. Ord v => Node v Index -> State (OBDD v) Index
register (Node v Index -> StateT (OBDD v) Identity Index)
-> Node v Index -> StateT (OBDD v) Identity Index
forall a b. (a -> b) -> a -> b
$ v -> Index -> Index -> Node v Index
forall v i. v -> i -> i -> Node v i
Branch v
v Index
l' Index
r'
    (StateT (IntMap Index) (StateT (OBDD v) Identity) Index
 -> IntMap Index -> State (OBDD v) Index)
-> IntMap Index
-> StateT (IntMap Index) (StateT (OBDD v) Identity) Index
-> State (OBDD v) Index
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (IntMap Index) (StateT (OBDD v) Identity) Index
-> IntMap Index -> State (OBDD v) Index
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
T.evalStateT IntMap Index
forall a. IntMap a
IM.empty (StateT (IntMap Index) (StateT (OBDD v) Identity) Index
 -> State (OBDD v) Index)
-> StateT (IntMap Index) (StateT (OBDD v) Identity) Index
-> State (OBDD v) Index
forall a b. (a -> b) -> a -> b
$ OBDD v -> StateT (IntMap Index) (StateT (OBDD v) Identity) Index
forall (t :: (* -> *) -> * -> *) v.
(MonadState (IntMap Index) (t (StateT (OBDD v) Identity)),
 MonadTrans t, Ord v) =>
OBDD v -> t (StateT (OBDD v) Identity) Index
handle OBDD v
x


data Symmetricity = Asymmetric | Symmetric deriving Index -> Symmetricity -> ShowS
[Symmetricity] -> ShowS
Symmetricity -> String
(Index -> Symmetricity -> ShowS)
-> (Symmetricity -> String)
-> ([Symmetricity] -> ShowS)
-> Show Symmetricity
forall a.
(Index -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Symmetricity] -> ShowS
$cshowList :: [Symmetricity] -> ShowS
show :: Symmetricity -> String
$cshow :: Symmetricity -> String
showsPrec :: Index -> Symmetricity -> ShowS
$cshowsPrec :: Index -> Symmetricity -> ShowS
Show

binary :: Ord v
      => ( Bool -> Bool -> Bool )
      -> OBDD v -> OBDD v -> OBDD v
binary :: (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
binary = Symmetricity
-> (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
forall v.
Ord v =>
Symmetricity
-> (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
binary_ Symmetricity
Asymmetric
      
symmetric_binary :: Ord v
      => ( Bool -> Bool -> Bool )
      -> OBDD v -> OBDD v -> OBDD v
symmetric_binary :: (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
symmetric_binary = Symmetricity
-> (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
forall v.
Ord v =>
Symmetricity
-> (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
binary_ Symmetricity
Symmetric

binary_ :: Ord v
      => Symmetricity
      -> ( Bool -> Bool -> Bool )
      -> OBDD v -> OBDD v -> OBDD v
-- FIXME https://github.com/jwaldmann/haskell-obdd/issues/4
binary_ :: Symmetricity
-> (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v
binary_ Symmetricity
_ Bool -> Bool -> Bool
op OBDD v
x OBDD v
y = State (OBDD v) Index -> OBDD v
forall v. State (OBDD v) Index -> OBDD v
make (State (OBDD v) Index -> OBDD v) -> State (OBDD v) Index -> OBDD v
forall a b. (a -> b) -> a -> b
$ do
    let -- register = checked_register -- for testing
        -- handle x y | Symmetric <- sym, top x > top y = handle y x
        handle :: OBDD v -> OBDD v -> t (StateT (OBDD v) Identity) Index
handle OBDD v
x OBDD v
y = (Index, Index)
-> t (StateT (OBDD v) Identity) Index
-> t (StateT (OBDD v) Identity) Index
forall (m :: * -> *) b.
MonadState (IntIntMap b) m =>
(Index, Index) -> m b -> m b
cachedIIM (OBDD v -> Index
forall v. OBDD v -> Index
top OBDD v
x, OBDD v -> Index
forall v. OBDD v -> Index
top OBDD v
y) (t (StateT (OBDD v) Identity) Index
 -> t (StateT (OBDD v) Identity) Index)
-> t (StateT (OBDD v) Identity) Index
-> t (StateT (OBDD v) Identity) Index
forall a b. (a -> b) -> a -> b
$ case ( OBDD v -> Node v (OBDD v)
forall v. OBDD v -> Node v (OBDD v)
access OBDD v
x , OBDD v -> Node v (OBDD v)
forall v. OBDD v -> Node v (OBDD v)
access OBDD v
y ) of
                    ( Leaf Bool
p , Leaf Bool
q ) -> do
                        StateT (OBDD v) Identity Index
-> t (StateT (OBDD v) Identity) Index
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
T.lift (StateT (OBDD v) Identity Index
 -> t (StateT (OBDD v) Identity) Index)
-> StateT (OBDD v) Identity Index
-> t (StateT (OBDD v) Identity) Index
forall a b. (a -> b) -> a -> b
$ Node v Index -> StateT (OBDD v) Identity Index
forall v. Ord v => Node v Index -> State (OBDD v) Index
register (Node v Index -> StateT (OBDD v) Identity Index)
-> Node v Index -> StateT (OBDD v) Identity Index
forall a b. (a -> b) -> a -> b
$ Bool -> Node v Index
forall v i. Bool -> Node v i
Leaf (Bool -> Node v Index) -> Bool -> Node v Index
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
op Bool
p Bool
q
                    ( Node v (OBDD v)
ax, Node v (OBDD v)
ay ) -> case Node v (OBDD v) -> Node v (OBDD v) -> Ordering
forall a i i. Ord a => Node a i -> Node a i -> Ordering
comp Node v (OBDD v)
ax Node v (OBDD v)
ay of
                        Ordering
LT -> do
                            let Branch v
v OBDD v
l OBDD v
r = Node v (OBDD v)
ay
                            Index
l' <- OBDD v -> OBDD v -> t (StateT (OBDD v) Identity) Index
handle OBDD v
x OBDD v
l
                            Index
r' <- OBDD v -> OBDD v -> t (StateT (OBDD v) Identity) Index
handle OBDD v
x OBDD v
r
                            StateT (OBDD v) Identity Index
-> t (StateT (OBDD v) Identity) Index
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
T.lift (StateT (OBDD v) Identity Index
 -> t (StateT (OBDD v) Identity) Index)
-> StateT (OBDD v) Identity Index
-> t (StateT (OBDD v) Identity) Index
forall a b. (a -> b) -> a -> b
$ Node v Index -> StateT (OBDD v) Identity Index
forall v. Ord v => Node v Index -> State (OBDD v) Index
register (Node v Index -> StateT (OBDD v) Identity Index)
-> Node v Index -> StateT (OBDD v) Identity Index
forall a b. (a -> b) -> a -> b
$ v -> Index -> Index -> Node v Index
forall v i. v -> i -> i -> Node v i
Branch v
v Index
l' Index
r'
                        Ordering
GT -> do
                            let Branch v
v OBDD v
l OBDD v
r = Node v (OBDD v)
ax
                            Index
l' <- OBDD v -> OBDD v -> t (StateT (OBDD v) Identity) Index
handle OBDD v
l OBDD v
y
                            Index
r' <- OBDD v -> OBDD v -> t (StateT (OBDD v) Identity) Index
handle OBDD v
r OBDD v
y
                            StateT (OBDD v) Identity Index
-> t (StateT (OBDD v) Identity) Index
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
T.lift (StateT (OBDD v) Identity Index
 -> t (StateT (OBDD v) Identity) Index)
-> StateT (OBDD v) Identity Index
-> t (StateT (OBDD v) Identity) Index
forall a b. (a -> b) -> a -> b
$ Node v Index -> StateT (OBDD v) Identity Index
forall v. Ord v => Node v Index -> State (OBDD v) Index
register (Node v Index -> StateT (OBDD v) Identity Index)
-> Node v Index -> StateT (OBDD v) Identity Index
forall a b. (a -> b) -> a -> b
$ v -> Index -> Index -> Node v Index
forall v i. v -> i -> i -> Node v i
Branch v
v Index
l' Index
r'
                        Ordering
EQ -> do
                            let Branch v
v1 OBDD v
l1 OBDD v
r1 = Node v (OBDD v)
ax
                                Branch v
v2 OBDD v
l2 OBDD v
r2 = Node v (OBDD v)
ay
                                v :: v
v = if v
v1 v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v2 then v
v1 else String -> v
forall a. HasCallStack => String -> a
error String
"OBDD.Operation.handle"
                            Index
l' <- OBDD v -> OBDD v -> t (StateT (OBDD v) Identity) Index
handle OBDD v
l1 OBDD v
l2
                            Index
r' <- OBDD v -> OBDD v -> t (StateT (OBDD v) Identity) Index
handle OBDD v
r1 OBDD v
r2
                            StateT (OBDD v) Identity Index
-> t (StateT (OBDD v) Identity) Index
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
T.lift (StateT (OBDD v) Identity Index
 -> t (StateT (OBDD v) Identity) Index)
-> StateT (OBDD v) Identity Index
-> t (StateT (OBDD v) Identity) Index
forall a b. (a -> b) -> a -> b
$ Node v Index -> StateT (OBDD v) Identity Index
forall v. Ord v => Node v Index -> State (OBDD v) Index
register (Node v Index -> StateT (OBDD v) Identity Index)
-> Node v Index -> StateT (OBDD v) Identity Index
forall a b. (a -> b) -> a -> b
$ v -> Index -> Index -> Node v Index
forall v i. v -> i -> i -> Node v i
Branch v
v Index
l' Index
r'
    (StateT (IntIntMap Index) (StateT (OBDD v) Identity) Index
 -> IntIntMap Index -> State (OBDD v) Index)
-> IntIntMap Index
-> StateT (IntIntMap Index) (StateT (OBDD v) Identity) Index
-> State (OBDD v) Index
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (IntIntMap Index) (StateT (OBDD v) Identity) Index
-> IntIntMap Index -> State (OBDD v) Index
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
T.evalStateT IntIntMap Index
forall v. IntIntMap v
IIM.empty (StateT (IntIntMap Index) (StateT (OBDD v) Identity) Index
 -> State (OBDD v) Index)
-> StateT (IntIntMap Index) (StateT (OBDD v) Identity) Index
-> State (OBDD v) Index
forall a b. (a -> b) -> a -> b
$ OBDD v
-> OBDD v
-> StateT (IntIntMap Index) (StateT (OBDD v) Identity) Index
forall (t :: (* -> *) -> * -> *) v.
(MonadState (IntIntMap Index) (t (StateT (OBDD v) Identity)),
 MonadTrans t, Ord v) =>
OBDD v -> OBDD v -> t (StateT (OBDD v) Identity) Index
handle OBDD v
x OBDD v
y

{-# inline cachedM #-}
cachedM :: k -> m b -> m b
cachedM k
arg m b
act = do
  Map k b
c <- m (Map k b)
forall s (m :: * -> *). MonadState s m => m s
T.get
  case k -> Map k b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
arg Map k b
c of
    Maybe b
Nothing -> do
      b
res <- m b
act ; (Map k b -> Map k b) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
T.modify' ((Map k b -> Map k b) -> m ()) -> (Map k b -> Map k b) -> m ()
forall a b. (a -> b) -> a -> b
$ k -> b -> Map k b -> Map k b
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert k
arg b
res; b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
res
    Just b
res -> do
      b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
res

{-# inline cachedIM #-}
cachedIM :: Index -> m b -> m b
cachedIM Index
arg m b
act = do
  IntMap b
c <- m (IntMap b)
forall s (m :: * -> *). MonadState s m => m s
T.get
  case Index -> IntMap b -> Maybe b
forall a. Index -> IntMap a -> Maybe a
IM.lookup Index
arg IntMap b
c of
    Maybe b
Nothing -> do
      b
res <- m b
act ; (IntMap b -> IntMap b) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
T.modify' ((IntMap b -> IntMap b) -> m ()) -> (IntMap b -> IntMap b) -> m ()
forall a b. (a -> b) -> a -> b
$ Index -> b -> IntMap b -> IntMap b
forall a. Index -> a -> IntMap a -> IntMap a
IM.insert Index
arg b
res; b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
res
    Just b
res -> do
      b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
res

{-# inline cachedIIM #-}
cachedIIM :: (Index, Index) -> m b -> m b
cachedIIM (Index, Index)
arg m b
act = do
  IntIntMap b
c <- m (IntIntMap b)
forall s (m :: * -> *). MonadState s m => m s
T.get
  case (Index, Index) -> IntIntMap b -> Maybe b
forall b. (Index, Index) -> IntIntMap b -> Maybe b
IIM.lookup (Index, Index)
arg IntIntMap b
c of
    Maybe b
Nothing -> do
      b
res <- m b
act ; (IntIntMap b -> IntIntMap b) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
T.modify' ((IntIntMap b -> IntIntMap b) -> m ())
-> (IntIntMap b -> IntIntMap b) -> m ()
forall a b. (a -> b) -> a -> b
$ (Index, Index) -> b -> IntIntMap b -> IntIntMap b
forall v. (Index, Index) -> v -> IntIntMap v -> IntIntMap v
IIM.insert (Index, Index)
arg b
res; b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
res
    Just b
res -> do
      b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
res

comp :: Node a i -> Node a i -> Ordering
comp Node a i
x Node a i
y = case (Node a i
x , Node a i
y) of
    ( Leaf {} , Leaf {} ) -> Ordering
EQ
    ( Branch {} , Leaf {} ) -> Ordering
GT
    ( Leaf {} , Branch {} ) ->  Ordering
LT
    ( Branch a
v1 i
_ i
_ , Branch a
v2 i
_ i
_ ) -> a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
v1 a
v2

-- | remove variables existentially
exists_many :: (Foldable c, Ord v)
            => c v
            -> OBDD v
            -> OBDD v
exists_many :: c v -> OBDD v -> OBDD v
exists_many c v
vars OBDD v
x =
    (v -> OBDD v -> OBDD v) -> OBDD v -> c v -> OBDD v
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr v -> OBDD v -> OBDD v
forall v. Ord v => v -> OBDD v -> OBDD v
exists OBDD v
x c v
vars 

-- | remove variable existentially
exists :: Ord v
      => v
      -> OBDD v -> OBDD v
exists :: v -> OBDD v -> OBDD v
exists v
var = (Bool -> OBDD v)
-> (v -> OBDD v -> OBDD v -> OBDD v) -> OBDD v -> OBDD v
forall v a.
Ord v =>
(Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a
fold Bool -> OBDD v
forall b. Boolean b => Bool -> b
bool
  ( \ v
v OBDD v
l OBDD v
r -> if v
var v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v then OBDD v
l OBDD v -> OBDD v -> OBDD v
forall b. Boolean b => b -> b -> b
|| OBDD v
r else OBDD v -> OBDD v -> OBDD v -> OBDD v
forall b. Boolean b => b -> b -> b -> b
choose OBDD v
l OBDD v
r (v -> OBDD v
forall v. Ord v => v -> OBDD v
variable v
v) )

forall_many :: (Foldable c, Ord v) => c v -> OBDD v -> OBDD v
forall_many :: c v -> OBDD v -> OBDD v
forall_many c v
vars OBDD v
x = 
    (v -> OBDD v -> OBDD v) -> OBDD v -> c v -> OBDD v
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr v -> OBDD v -> OBDD v
forall v. Ord v => v -> OBDD v -> OBDD v
forall OBDD v
x c v
vars 

forall :: Ord v => v -> OBDD v -> OBDD v
forall :: v -> OBDD v -> OBDD v
forall v
var = (Bool -> OBDD v)
-> (v -> OBDD v -> OBDD v -> OBDD v) -> OBDD v -> OBDD v
forall v a.
Ord v =>
(Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a
fold Bool -> OBDD v
forall b. Boolean b => Bool -> b
bool
  ( \ v
v OBDD v
l OBDD v
r -> if v
var v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v then OBDD v
l OBDD v -> OBDD v -> OBDD v
forall b. Boolean b => b -> b -> b
&& OBDD v
r else OBDD v -> OBDD v -> OBDD v -> OBDD v
forall b. Boolean b => b -> b -> b -> b
choose OBDD v
l OBDD v
r (v -> OBDD v
forall v. Ord v => v -> OBDD v
variable v
v) )

-- | replace variable by value
instantiate :: Ord v => 
            v -> Bool 
            -> OBDD v
            -> OBDD v
instantiate :: v -> Bool -> OBDD v -> OBDD v
instantiate v
var Bool
val = (Bool -> OBDD v)
-> (v -> OBDD v -> OBDD v -> OBDD v) -> OBDD v -> OBDD v
forall v a.
Ord v =>
(Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a
fold Bool -> OBDD v
forall b. Boolean b => Bool -> b
bool
  ( \ v
v OBDD v
l OBDD v
r ->
    if v
var v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v then OBDD v -> OBDD v -> Bool -> OBDD v
forall a. a -> a -> Bool -> a
Data.Bool.bool OBDD v
l OBDD v
r Bool
val
    else OBDD v -> OBDD v -> OBDD v -> OBDD v
forall b. Boolean b => b -> b -> b -> b
choose OBDD v
l OBDD v
r (v -> OBDD v
forall v. Ord v => v -> OBDD v
variable v
v) )