{-# language GeneralizedNewtypeDeriving #-}
{-# language RecursiveDo #-}
{-# language FlexibleContexts #-}
{-# language TupleSections #-}
module OBDD.Data
(
OBDD
, size
, null, satisfiable
, number_of_models
, variables, paths, models
, some_model
, fold, foldM
, full_fold, full_foldM
, Node (..)
, make
, register, checked_register
, top
, access
, not_
, assocs
)
where
import Data.IntMap.Strict ( IntMap )
import qualified Data.IntMap.Strict as IM
import OBDD.IntIntMap (IntIntMap)
import qualified OBDD.IntIntMap as IIM
import OBDD.VarIntIntMap (VarIntIntMap)
import qualified OBDD.VarIntIntMap as VIIM
import Data.Map.Strict ( Map )
import qualified Data.Map.Strict as M
import qualified Data.Array as A
import Data.Set ( Set )
import qualified Data.Set as S
import Data.Bool (bool)
import Control.Arrow ( (&&&) )
import Control.Monad.State.Strict
(State, runState, evalState, get, put, gets, modify)
import qualified System.Random
import Control.Monad.Fix
import Control.Monad ( forM, guard, void )
import qualified Control.Monad ( foldM )
import Data.Functor.Identity
import Data.List (isPrefixOf, isSuffixOf)
import Prelude hiding ( null )
import qualified Prelude
type Index = Int ; unIndex :: a -> a
unIndex = a -> a
forall a. a -> a
id
data OBDD v = OBDD
{ OBDD v -> IntMap (Node v Index)
core :: !(IntMap ( Node v Index ))
, OBDD v -> VarIntIntMap v Index
icore :: !(VarIntIntMap v Index)
, OBDD v -> Index
ifalse :: !Index
, OBDD v -> Index
itrue :: !Index
, OBDD v -> Index
next :: !Index
, OBDD v -> Index
top :: !Index
}
assocs :: OBDD v -> [(Index, Node v Index)]
assocs :: OBDD v -> [(Index, Node v Index)]
assocs OBDD v
o = IntMap (Node v Index) -> [(Index, Node v Index)]
forall a. IntMap a -> [(Index, a)]
IM.toAscList (IntMap (Node v Index) -> [(Index, Node v Index)])
-> IntMap (Node v Index) -> [(Index, Node v Index)]
forall a b. (a -> b) -> a -> b
$ OBDD v -> IntMap (Node v Index)
forall v. OBDD v -> IntMap (Node v Index)
core OBDD v
o
fold :: Ord v
=> ( Bool -> a )
-> ( v -> a -> a -> a )
-> OBDD v -> a
fold :: (Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a
fold Bool -> a
leaf v -> a -> a -> a
branch OBDD v
o = Identity a -> a
forall a. Identity a -> a
runIdentity
(Identity a -> a) -> Identity a -> a
forall a b. (a -> b) -> a -> b
$ (Bool -> Identity a)
-> (v -> a -> a -> Identity a) -> OBDD v -> Identity a
forall (m :: * -> *) v a.
(Monad m, Ord v) =>
(Bool -> m a) -> (v -> a -> a -> m a) -> OBDD v -> m a
foldM ( a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Identity a) -> (Bool -> a) -> Bool -> Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> a
leaf )
( \ v
v a
l a
r -> a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Identity a) -> a -> Identity a
forall a b. (a -> b) -> a -> b
$ v -> a -> a -> a
branch v
v a
l a
r )
OBDD v
o
foldM :: (Monad m, Ord v)
=> ( Bool -> m a )
-> ( v -> a -> a -> m a )
-> OBDD v -> m a
foldM :: (Bool -> m a) -> (v -> a -> a -> m a) -> OBDD v -> m a
foldM Bool -> m a
leaf v -> a -> a -> m a
branch OBDD v
o = do
Map Index a
m <- (Map Index a -> (Index, Node v Index) -> m (Map Index a))
-> Map Index a -> [(Index, Node v Index)] -> m (Map Index a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
Control.Monad.foldM ( \ Map Index a
m (Index
i,Node v Index
n) -> do
a
val <- case Node v Index
n of
Leaf Bool
b -> Bool -> m a
leaf Bool
b
Branch v
v Index
l Index
r ->
v -> a -> a -> m a
branch v
v (Map Index a
m Map Index a -> Index -> a
forall k a. Ord k => Map k a -> k -> a
M.! Index
l) (Map Index a
m Map Index a -> Index -> a
forall k a. Ord k => Map k a -> k -> a
M.! Index
r)
Map Index a -> m (Map Index a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Index a -> m (Map Index a)) -> Map Index a -> m (Map Index a)
forall a b. (a -> b) -> a -> b
$ Index -> a -> Map Index a -> Map Index a
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Index
i a
val Map Index a
m
) Map Index a
forall k a. Map k a
M.empty ([(Index, Node v Index)] -> m (Map Index a))
-> [(Index, Node v Index)] -> m (Map Index a)
forall a b. (a -> b) -> a -> b
$ IntMap (Node v Index) -> [(Index, Node v Index)]
forall a. IntMap a -> [(Index, a)]
IM.toAscList (IntMap (Node v Index) -> [(Index, Node v Index)])
-> IntMap (Node v Index) -> [(Index, Node v Index)]
forall a b. (a -> b) -> a -> b
$ OBDD v -> IntMap (Node v Index)
forall v. OBDD v -> IntMap (Node v Index)
core OBDD v
o
a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ Map Index a
m Map Index a -> Index -> a
forall k a. Ord k => Map k a -> k -> a
M.! OBDD v -> Index
forall v. OBDD v -> Index
top OBDD v
o
full_fold :: Ord v
=> Set v
-> ( Bool -> a )
-> ( v -> a -> a -> a )
-> OBDD v -> a
full_fold :: Set v -> (Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a
full_fold Set v
vars Bool -> a
leaf v -> a -> a -> a
branch OBDD v
o = Identity a -> a
forall a. Identity a -> a
runIdentity
(Identity a -> a) -> Identity a -> a
forall a b. (a -> b) -> a -> b
$ Set v
-> (Bool -> Identity a)
-> (v -> a -> a -> Identity a)
-> OBDD v
-> Identity a
forall (m :: * -> *) v a.
(Monad m, Ord v) =>
Set v -> (Bool -> m a) -> (v -> a -> a -> m a) -> OBDD v -> m a
full_foldM Set v
vars
( a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Identity a) -> (Bool -> a) -> Bool -> Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> a
leaf )
( \ v
v a
l a
r -> a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Identity a) -> a -> Identity a
forall a b. (a -> b) -> a -> b
$ v -> a -> a -> a
branch v
v a
l a
r )
OBDD v
o
full_foldM :: (Monad m, Ord v)
=> Set v
-> ( Bool -> m a )
-> ( v -> a -> a -> m a )
-> OBDD v -> m a
full_foldM :: Set v -> (Bool -> m a) -> (v -> a -> a -> m a) -> OBDD v -> m a
full_foldM Set v
vars Bool -> m a
leaf v -> a -> a -> m a
branch OBDD v
o = do
let vs :: [v]
vs = Set v -> [v]
forall a. Set a -> [a]
S.toAscList (Set v -> [v]) -> Set v -> [v]
forall a b. (a -> b) -> a -> b
$ Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
S.union (OBDD v -> Set v
forall v. Ord v => OBDD v -> Set v
variables OBDD v
o) Set v
vars
low :: v
low = [v] -> v
forall a. [a] -> a
head [v]
vs
m :: Map v v
m = [(v, v)] -> Map v v
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(v, v)] -> Map v v) -> [(v, v)] -> Map v v
forall a b. (a -> b) -> a -> b
$ [v] -> [v] -> [(v, v)]
forall a b. [a] -> [b] -> [(a, b)]
zip [v]
vs ([v] -> [(v, v)]) -> [v] -> [(v, v)]
forall a b. (a -> b) -> a -> b
$ [v] -> [v]
forall a. [a] -> [a]
tail [v]
vs
up :: v -> Maybe v
up v
v = v -> Map v v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup v
v Map v v
m
interpolate :: Maybe v -> Maybe v -> a -> m a
interpolate Maybe v
now Maybe v
goal a
x | Maybe v
now Maybe v -> Maybe v -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe v
goal = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
interpolate (Just v
now) Maybe v
goal a
x =
v -> a -> a -> m a
branch v
now a
x a
x m a -> (a -> m a) -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Maybe v -> Maybe v -> a -> m a
interpolate (v -> Maybe v
up v
now) Maybe v
goal
(Maybe v
a,a
res) <- (Bool -> m (Maybe v, a))
-> (v -> (Maybe v, a) -> (Maybe v, a) -> m (Maybe v, a))
-> OBDD v
-> m (Maybe v, a)
forall (m :: * -> *) v a.
(Monad m, Ord v) =>
(Bool -> m a) -> (v -> a -> a -> m a) -> OBDD v -> m a
foldM
( \ Bool
b -> (v -> Maybe v
forall a. a -> Maybe a
Just v
low ,) (a -> (Maybe v, a)) -> m a -> m (Maybe v, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> m a
leaf Bool
b )
( \ v
v (Maybe v
p,a
l) (Maybe v
q,a
r) -> do
a
l' <- Maybe v -> Maybe v -> a -> m a
interpolate Maybe v
p (v -> Maybe v
forall a. a -> Maybe a
Just v
v) a
l
a
r' <- Maybe v -> Maybe v -> a -> m a
interpolate Maybe v
q (v -> Maybe v
forall a. a -> Maybe a
Just v
v) a
r
(v -> Maybe v
up v
v,) (a -> (Maybe v, a)) -> m a -> m (Maybe v, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> v -> a -> a -> m a
branch v
v a
l' a
r'
) OBDD v
o
Maybe v -> Maybe v -> a -> m a
interpolate Maybe v
a Maybe v
forall a. Maybe a
Nothing a
res
size :: OBDD v -> Index
size = Index -> Index
forall a. a -> a
unIndex (Index -> Index) -> (OBDD v -> Index) -> OBDD v -> Index
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OBDD v -> Index
forall v. OBDD v -> Index
next
number_of_models :: Ord v => Set v -> OBDD v -> Integer
number_of_models :: Set v -> OBDD v -> Integer
number_of_models Set v
vars OBDD v
o =
Set v
-> (Bool -> Integer)
-> (v -> Integer -> Integer -> Integer)
-> OBDD v
-> Integer
forall v a.
Ord v =>
Set v -> (Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a
full_fold Set v
vars (Integer -> Integer -> Bool -> Integer
forall a. a -> a -> Bool -> a
bool Integer
0 Integer
1) ( (Integer -> Integer -> Integer)
-> v -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) ) OBDD v
o
empty :: OBDD v
empty :: OBDD v
empty = OBDD :: forall v.
IntMap (Node v Index)
-> VarIntIntMap v Index
-> Index
-> Index
-> Index
-> Index
-> OBDD v
OBDD
{ core :: IntMap (Node v Index)
core = [(Index, Node v Index)] -> IntMap (Node v Index)
forall a. [(Index, a)] -> IntMap a
IM.fromList [(Index
0,Bool -> Node v Index
forall v i. Bool -> Node v i
Leaf Bool
False),(Index
1,Bool -> Node v Index
forall v i. Bool -> Node v i
Leaf Bool
True)]
, icore :: VarIntIntMap v Index
icore = VarIntIntMap v Index
forall k v. VarIntIntMap k v
VIIM.empty
, ifalse :: Index
ifalse = Index
0
, itrue :: Index
itrue = Index
1
, next :: Index
next = Index
2
, top :: Index
top = -Index
1
}
data Node v i = Leaf !Bool
| Branch !v !i !i
deriving ( Node v i -> Node v i -> Bool
(Node v i -> Node v i -> Bool)
-> (Node v i -> Node v i -> Bool) -> Eq (Node v i)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall v i. (Eq v, Eq i) => Node v i -> Node v i -> Bool
/= :: Node v i -> Node v i -> Bool
$c/= :: forall v i. (Eq v, Eq i) => Node v i -> Node v i -> Bool
== :: Node v i -> Node v i -> Bool
$c== :: forall v i. (Eq v, Eq i) => Node v i -> Node v i -> Bool
Eq, Eq (Node v i)
Eq (Node v i)
-> (Node v i -> Node v i -> Ordering)
-> (Node v i -> Node v i -> Bool)
-> (Node v i -> Node v i -> Bool)
-> (Node v i -> Node v i -> Bool)
-> (Node v i -> Node v i -> Bool)
-> (Node v i -> Node v i -> Node v i)
-> (Node v i -> Node v i -> Node v i)
-> Ord (Node v i)
Node v i -> Node v i -> Bool
Node v i -> Node v i -> Ordering
Node v i -> Node v i -> Node v i
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall v i. (Ord v, Ord i) => Eq (Node v i)
forall v i. (Ord v, Ord i) => Node v i -> Node v i -> Bool
forall v i. (Ord v, Ord i) => Node v i -> Node v i -> Ordering
forall v i. (Ord v, Ord i) => Node v i -> Node v i -> Node v i
min :: Node v i -> Node v i -> Node v i
$cmin :: forall v i. (Ord v, Ord i) => Node v i -> Node v i -> Node v i
max :: Node v i -> Node v i -> Node v i
$cmax :: forall v i. (Ord v, Ord i) => Node v i -> Node v i -> Node v i
>= :: Node v i -> Node v i -> Bool
$c>= :: forall v i. (Ord v, Ord i) => Node v i -> Node v i -> Bool
> :: Node v i -> Node v i -> Bool
$c> :: forall v i. (Ord v, Ord i) => Node v i -> Node v i -> Bool
<= :: Node v i -> Node v i -> Bool
$c<= :: forall v i. (Ord v, Ord i) => Node v i -> Node v i -> Bool
< :: Node v i -> Node v i -> Bool
$c< :: forall v i. (Ord v, Ord i) => Node v i -> Node v i -> Bool
compare :: Node v i -> Node v i -> Ordering
$ccompare :: forall v i. (Ord v, Ord i) => Node v i -> Node v i -> Ordering
$cp1Ord :: forall v i. (Ord v, Ord i) => Eq (Node v i)
Ord )
not_ :: OBDD v -> OBDD v
not_ OBDD v
o = OBDD v
o { ifalse :: Index
ifalse = OBDD v -> Index
forall v. OBDD v -> Index
itrue OBDD v
o
, itrue :: Index
itrue = OBDD v -> Index
forall v. OBDD v -> Index
ifalse OBDD v
o
, core :: IntMap (Node v Index)
core = Index
-> Node v Index -> IntMap (Node v Index) -> IntMap (Node v Index)
forall a. Index -> a -> IntMap a -> IntMap a
IM.insert (OBDD v -> Index
forall v. OBDD v -> Index
itrue OBDD v
o) (Bool -> Node v Index
forall v i. Bool -> Node v i
Leaf Bool
False)
(IntMap (Node v Index) -> IntMap (Node v Index))
-> IntMap (Node v Index) -> IntMap (Node v Index)
forall a b. (a -> b) -> a -> b
$ Index
-> Node v Index -> IntMap (Node v Index) -> IntMap (Node v Index)
forall a. Index -> a -> IntMap a -> IntMap a
IM.insert (OBDD v -> Index
forall v. OBDD v -> Index
ifalse OBDD v
o) (Bool -> Node v Index
forall v i. Bool -> Node v i
Leaf Bool
True)
(IntMap (Node v Index) -> IntMap (Node v Index))
-> IntMap (Node v Index) -> IntMap (Node v Index)
forall a b. (a -> b) -> a -> b
$ OBDD v -> IntMap (Node v Index)
forall v. OBDD v -> IntMap (Node v Index)
core OBDD v
o
}
access :: OBDD v -> Node v ( OBDD v )
access :: OBDD v -> Node v (OBDD v)
access OBDD v
s = case OBDD v -> Index
forall v. OBDD v -> Index
top OBDD v
s of
Index
i | Index
i Index -> Index -> Bool
forall a. Eq a => a -> a -> Bool
== OBDD v -> Index
forall v. OBDD v -> Index
ifalse OBDD v
s -> Bool -> Node v (OBDD v)
forall v i. Bool -> Node v i
Leaf Bool
False
Index
i | Index
i Index -> Index -> Bool
forall a. Eq a => a -> a -> Bool
== OBDD v -> Index
forall v. OBDD v -> Index
itrue OBDD v
s -> Bool -> Node v (OBDD v)
forall v i. Bool -> Node v i
Leaf Bool
True
Index
t -> case Index -> IntMap (Node v Index) -> Maybe (Node v Index)
forall a. Index -> IntMap a -> Maybe a
IM.lookup ( OBDD v -> Index
forall v. OBDD v -> Index
top OBDD v
s ) ( OBDD v -> IntMap (Node v Index)
forall v. OBDD v -> IntMap (Node v Index)
core OBDD v
s ) of
Maybe (Node v Index)
Nothing -> [Char] -> Node v (OBDD v)
forall a. HasCallStack => [Char] -> a
error [Char]
"OBDD.Data.access"
Just Node v Index
n -> case Node v Index
n of
Leaf Bool
p -> [Char] -> Node v (OBDD v)
forall a. HasCallStack => [Char] -> a
error [Char]
"Leaf in core"
Branch v
v Index
l Index
r ->
v -> OBDD v -> OBDD v -> Node v (OBDD v)
forall v i. v -> i -> i -> Node v i
Branch v
v ( OBDD v
s { top :: Index
top = Index
l } )
( OBDD v
s { top :: Index
top = Index
r } )
satisfiable :: OBDD v -> Bool
satisfiable :: OBDD v -> Bool
satisfiable = Bool -> Bool
not (Bool -> Bool) -> (OBDD v -> Bool) -> OBDD v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OBDD v -> Bool
forall v. OBDD v -> Bool
null
null :: OBDD v -> Bool
null :: OBDD v -> Bool
null OBDD v
s = case OBDD v -> Node v (OBDD v)
forall v. OBDD v -> Node v (OBDD v)
access OBDD v
s of
Leaf Bool
False -> Bool
True
Node v (OBDD v)
_ -> Bool
False
some_model :: Ord v
=> OBDD v
-> IO ( Maybe ( Map v Bool ) )
some_model :: OBDD v -> IO (Maybe (Map v Bool))
some_model OBDD v
s = case OBDD v -> Node v (OBDD v)
forall v. OBDD v -> Node v (OBDD v)
access OBDD v
s of
Leaf Bool
True -> Maybe (Map v Bool) -> IO (Maybe (Map v Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Map v Bool) -> IO (Maybe (Map v Bool)))
-> Maybe (Map v Bool) -> IO (Maybe (Map v Bool))
forall a b. (a -> b) -> a -> b
$ Map v Bool -> Maybe (Map v Bool)
forall a. a -> Maybe a
Just (Map v Bool -> Maybe (Map v Bool))
-> Map v Bool -> Maybe (Map v Bool)
forall a b. (a -> b) -> a -> b
$ Map v Bool
forall k a. Map k a
M.empty
Leaf Bool
False -> Maybe (Map v Bool) -> IO (Maybe (Map v Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Map v Bool)
forall a. Maybe a
Nothing
Branch v
v OBDD v
l OBDD v
r -> do
let nonempty_children :: [(Bool, OBDD v)]
nonempty_children = do
( Bool
p, OBDD v
t ) <- [ (Bool
False, OBDD v
l), (Bool
True, OBDD v
r) ]
Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
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
t of
Leaf Bool
False -> Bool
False
Node v (OBDD v)
_ -> Bool
True
(Bool, OBDD v) -> [(Bool, OBDD v)]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Bool
p, OBDD v
t )
(Bool
p, OBDD v
t) <- [(Bool, OBDD v)] -> IO (Bool, OBDD v)
forall a. [a] -> IO a
select_one [(Bool, OBDD v)]
nonempty_children
Just Map v Bool
m <- OBDD v -> IO (Maybe (Map v Bool))
forall v. Ord v => OBDD v -> IO (Maybe (Map v Bool))
some_model OBDD v
t
Maybe (Map v Bool) -> IO (Maybe (Map v Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Map v Bool) -> IO (Maybe (Map v Bool)))
-> Maybe (Map v Bool) -> IO (Maybe (Map v Bool))
forall a b. (a -> b) -> a -> b
$ Map v Bool -> Maybe (Map v Bool)
forall a. a -> Maybe a
Just (Map v Bool -> Maybe (Map v Bool))
-> Map v Bool -> Maybe (Map v Bool)
forall a b. (a -> b) -> a -> b
$ v -> Bool -> Map v Bool -> Map v Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert v
v Bool
p Map v Bool
m
variables :: Ord v => OBDD v -> S.Set v
variables :: OBDD v -> Set v
variables OBDD v
f = (Bool -> Set v)
-> (v -> Set v -> Set v -> Set v) -> OBDD v -> Set v
forall v a.
Ord v =>
(Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a
fold (\ Bool
b -> Set v
forall a. Set a
S.empty )
( \ v
v Set v
l Set v
r -> v -> Set v -> Set v
forall a. Ord a => a -> Set a -> Set a
S.insert v
v (Set v -> Set v) -> Set v -> Set v
forall a b. (a -> b) -> a -> b
$ Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
S.union Set v
l Set v
r ) OBDD v
f
paths :: Ord v => OBDD v -> [ Map v Bool ]
paths :: OBDD v -> [Map v Bool]
paths =
(Bool -> [Map v Bool])
-> (v -> [Map v Bool] -> [Map v Bool] -> [Map v Bool])
-> OBDD v
-> [Map v Bool]
forall v a.
Ord v =>
(Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a
fold ( [Map v Bool] -> [Map v Bool] -> Bool -> [Map v Bool]
forall a. a -> a -> Bool -> a
bool [] [ Map v Bool
forall k a. Map k a
M.empty ] )
( \ v
v [Map v Bool]
l [Map v Bool]
r -> (v -> Bool -> Map v Bool -> Map v Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert v
v Bool
False (Map v Bool -> Map v Bool) -> [Map v Bool] -> [Map v Bool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Map v Bool]
l)
[Map v Bool] -> [Map v Bool] -> [Map v Bool]
forall a. [a] -> [a] -> [a]
++ (v -> Bool -> Map v Bool -> Map v Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert v
v Bool
True (Map v Bool -> Map v Bool) -> [Map v Bool] -> [Map v Bool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Map v Bool]
r) )
models :: Set k -> OBDD k -> [Map k Bool]
models Set k
vars =
Set k
-> (Bool -> [Map k Bool])
-> (k -> [Map k Bool] -> [Map k Bool] -> [Map k Bool])
-> OBDD k
-> [Map k Bool]
forall v a.
Ord v =>
Set v -> (Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a
full_fold Set k
vars ( [Map k Bool] -> [Map k Bool] -> Bool -> [Map k Bool]
forall a. a -> a -> Bool -> a
bool [] [ Map k Bool
forall k a. Map k a
M.empty ] )
( \ k
v [Map k Bool]
l [Map k Bool]
r -> (k -> Bool -> Map k Bool -> Map k Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert k
v Bool
False (Map k Bool -> Map k Bool) -> [Map k Bool] -> [Map k Bool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Map k Bool]
l)
[Map k Bool] -> [Map k Bool] -> [Map k Bool]
forall a. [a] -> [a] -> [a]
++ (k -> Bool -> Map k Bool -> Map k Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert k
v Bool
True (Map k Bool -> Map k Bool) -> [Map k Bool] -> [Map k Bool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Map k Bool]
r) )
select_one :: [a] -> IO a
select_one :: [a] -> IO a
select_one [a]
xs | Bool -> Bool
not ( [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Prelude.null [a]
xs ) = do
Index
i <- (Index, Index) -> IO Index
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
System.Random.randomRIO ( Index
0, [a] -> Index
forall (t :: * -> *) a. Foldable t => t a -> Index
length [a]
xs Index -> Index -> Index
forall a. Num a => a -> a -> a
- Index
1 )
a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> IO a) -> a -> IO a
forall a b. (a -> b) -> a -> b
$ [a]
xs [a] -> Index -> a
forall a. [a] -> Index -> a
!! Index
i
make :: State ( OBDD v ) Index
-> OBDD v
make :: State (OBDD v) Index -> OBDD v
make State (OBDD v) Index
action =
let ( Index
i, OBDD v
s ) = State (OBDD v) Index -> OBDD v -> (Index, OBDD v)
forall s a. State s a -> s -> (a, s)
runState State (OBDD v) Index
action OBDD v
forall v. OBDD v
empty
in Index
i Index -> OBDD v -> OBDD v
`seq` OBDD v
s { top :: Index
top = Index
i }
fresh :: State ( OBDD v ) Index
fresh :: State (OBDD v) Index
fresh = do
OBDD v
s <- StateT (OBDD v) Identity (OBDD v)
forall s (m :: * -> *). MonadState s m => m s
get
let i :: Index
i = OBDD v -> Index
forall v. OBDD v -> Index
next OBDD v
s
OBDD v -> StateT (OBDD v) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (OBDD v -> StateT (OBDD v) Identity ())
-> OBDD v -> StateT (OBDD v) Identity ()
forall a b. (a -> b) -> a -> b
$! OBDD v
s { next :: Index
next = Index -> Index
forall a. Enum a => a -> a
succ Index
i }
Index -> State (OBDD v) Index
forall (m :: * -> *) a. Monad m => a -> m a
return Index
i
register :: Ord v
=> Node v Index
-> State ( OBDD v ) Index
register :: Node v Index -> State (OBDD v) Index
register Node v Index
n = case Node v Index
n of
Leaf Bool
False -> OBDD v -> Index
forall v. OBDD v -> Index
ifalse (OBDD v -> Index)
-> StateT (OBDD v) Identity (OBDD v) -> State (OBDD v) Index
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (OBDD v) Identity (OBDD v)
forall s (m :: * -> *). MonadState s m => m s
get
Leaf Bool
True -> OBDD v -> Index
forall v. OBDD v -> Index
itrue (OBDD v -> Index)
-> StateT (OBDD v) Identity (OBDD v) -> State (OBDD v) Index
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (OBDD v) Identity (OBDD v)
forall s (m :: * -> *). MonadState s m => m s
get
Branch v
v Index
l Index
r -> if Index
l Index -> Index -> Bool
forall a. Eq a => a -> a -> Bool
== Index
r then Index -> State (OBDD v) Index
forall (m :: * -> *) a. Monad m => a -> m a
return Index
l else do
OBDD v
s <- StateT (OBDD v) Identity (OBDD v)
forall s (m :: * -> *). MonadState s m => m s
get
case (v, Index, Index) -> VarIntIntMap v Index -> Maybe Index
forall k b.
Ord k =>
(k, Index, Index) -> VarIntIntMap k b -> Maybe b
VIIM.lookup (v
v, Index
l, Index
r) ( OBDD v -> VarIntIntMap v Index
forall v. OBDD v -> VarIntIntMap v Index
icore OBDD v
s ) of
Just Index
i -> Index -> State (OBDD v) Index
forall (m :: * -> *) a. Monad m => a -> m a
return Index
i
Maybe Index
Nothing -> do
Index
i <- State (OBDD v) Index
forall v. State (OBDD v) Index
fresh
OBDD v
s <- StateT (OBDD v) Identity (OBDD v)
forall s (m :: * -> *). MonadState s m => m s
get
OBDD v -> StateT (OBDD v) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (OBDD v -> StateT (OBDD v) Identity ())
-> OBDD v -> StateT (OBDD v) Identity ()
forall a b. (a -> b) -> a -> b
$! OBDD v
s
{ core :: IntMap (Node v Index)
core = Index
-> Node v Index -> IntMap (Node v Index) -> IntMap (Node v Index)
forall a. Index -> a -> IntMap a -> IntMap a
IM.insert Index
i Node v Index
n (IntMap (Node v Index) -> IntMap (Node v Index))
-> IntMap (Node v Index) -> IntMap (Node v Index)
forall a b. (a -> b) -> a -> b
$ OBDD v -> IntMap (Node v Index)
forall v. OBDD v -> IntMap (Node v Index)
core OBDD v
s
, icore :: VarIntIntMap v Index
icore = (v, Index, Index)
-> Index -> VarIntIntMap v Index -> VarIntIntMap v Index
forall k v.
Ord k =>
(k, Index, Index) -> v -> VarIntIntMap k v -> VarIntIntMap k v
VIIM.insert (v
v, Index
l, Index
r) Index
i
(VarIntIntMap v Index -> VarIntIntMap v Index)
-> VarIntIntMap v Index -> VarIntIntMap v Index
forall a b. (a -> b) -> a -> b
$ OBDD v -> VarIntIntMap v Index
forall v. OBDD v -> VarIntIntMap v Index
icore OBDD v
s
}
Index -> State (OBDD v) Index
forall (m :: * -> *) a. Monad m => a -> m a
return Index
i
checked_register :: Ord v
=> Node v Index
-> State ( OBDD v ) Index
checked_register :: Node v Index -> State (OBDD v) Index
checked_register Node v Index
n = case Node v Index
n of
Branch v
v Index
l Index
r -> do
OBDD v
s <- StateT (OBDD v) Identity (OBDD v)
forall s (m :: * -> *). MonadState s m => m s
get
let check_var_ordering :: Index -> m ()
check_var_ordering Index
b = case Index -> IntMap (Node v Index) -> Maybe (Node v Index)
forall a. Index -> IntMap a -> Maybe a
IM.lookup Index
b (OBDD v -> IntMap (Node v Index)
forall v. OBDD v -> IntMap (Node v Index)
core OBDD v
s ) of
Just (Branch v
av Index
_ Index
_) | Bool -> Bool
not (v
v v -> v -> Bool
forall a. Ord a => a -> a -> Bool
> v
av) ->
[Char] -> m ()
forall a. HasCallStack => [Char] -> a
error [Char]
"wrong variable ordering"
Maybe (Node v Index)
_ -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Index -> StateT (OBDD v) Identity ()
forall (m :: * -> *). Monad m => Index -> m ()
check_var_ordering Index
l ; Index -> StateT (OBDD v) Identity ()
forall (m :: * -> *). Monad m => Index -> m ()
check_var_ordering Index
r
Node v Index -> State (OBDD v) Index
forall v. Ord v => Node v Index -> State (OBDD v) Index
register Node v Index
n
Node v Index
_ -> Node v Index -> State (OBDD v) Index
forall v. Ord v => Node v Index -> State (OBDD v) Index
register Node v Index
n