{-# language GeneralizedNewtypeDeriving #-}
{-# language RecursiveDo #-}
{-# language FlexibleContexts #-}
{-# language TupleSections #-}

-- | implementation of reduced ordered binary decision diagrams.

module OBDD.Data 

(
-- * the data type
 OBDD -- abstract
, size
-- * for external use
, null, satisfiable
, number_of_models
, variables, paths, models
, some_model
, fold, foldM
, full_fold, full_foldM
-- * for internal use
, 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

-- newtype Index = Index { unIndex :: Int }
--   deriving ( Eq, Ord, Num, Enum, Show )

type Index = Int ; unIndex :: a -> a
unIndex = a -> a
forall a. a -> a
id

-- | assumes total ordering on variables
data OBDD v = OBDD
            { OBDD v -> IntMap (Node v Index)
core :: !(IntMap ( Node v Index ))
            
            -- , icore :: !(Map ( Node v Index ) 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

-- | Apply function in each node, bottom-up.
-- return the value in the root node.
-- Will cache intermediate results.
-- You might think that 
-- @count_models = fold (\b -> if b then 1 else 0) (\v l r -> l + r)@ 
-- but that's not true because a path might omit variables.
-- Use @full_fold@ to fold over interpolated nodes as well.
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

-- | Run action in each node, bottum-up.
-- return the value in the root node.
-- Will cache intermediate results.
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

-- | Apply function in each node, bottom-up.
-- Also apply to interpolated nodes: when a link
-- from a node to a child skips some variables:
-- for each skipped variable, we run the @branch@ function
-- on an interpolated node that contains this missing variable,
-- and identical children.
-- With this function, @number_of_models@
-- can be implemented as 
-- @full_fold vars (bool 0 1) ( const (+) )@.
-- And it actually is, see the source.
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 satisfying assignments with  given set of variables.
-- The set of variables must be given since the current OBDD may not contain
-- all variables that were used to construct it, since some  nodes may have been removed
-- because they had identical children.
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 } )

-- | does the OBDD have any models?
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

-- | does the OBDD not have any models?
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

-- | randomly select one model, if possible
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 

-- | all variables that occur in the nodes
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

-- | list of all paths
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) )

-- | list of all models (a.k.a. minterms)
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