-- | builds basic OBDDs

module OBDD.Make 

( constant, unit, variable )

where

import OBDD.Data

import Data.Map ( Map )
import qualified Data.Map as M

constant :: Ord v => Bool -> OBDD v
constant :: Bool -> OBDD v
constant Bool
b = 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
    Node v Index -> State (OBDD v) Index
forall v. Ord v => Node v Index -> State (OBDD v) Index
register (Node v Index -> State (OBDD v) Index)
-> Node v Index -> State (OBDD v) Index
forall a b. (a -> b) -> a -> b
$ Bool -> Node v Index
forall v i. Bool -> Node v i
Leaf Bool
b

-- | Variable with given parity
unit :: Ord v => v -> Bool -> OBDD v
unit :: v -> Bool -> OBDD v
unit v
v Bool
p = 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
    Index
l <- Node v Index -> State (OBDD v) Index
forall v. Ord v => Node v Index -> State (OBDD v) Index
register (Node v Index -> State (OBDD v) Index)
-> Node v Index -> State (OBDD v) 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
not Bool
p
    Index
r <- Node v Index -> State (OBDD v) Index
forall v. Ord v => Node v Index -> State (OBDD v) Index
register (Node v Index -> State (OBDD v) Index)
-> Node v Index -> State (OBDD v) 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
p
    Node v Index -> State (OBDD v) Index
forall v. Ord v => Node v Index -> State (OBDD v) Index
register (Node v Index -> State (OBDD v) Index)
-> Node v Index -> State (OBDD v) 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

variable :: Ord v => v -> OBDD v
variable :: v -> OBDD v
variable v
v = v -> Bool -> OBDD v
forall v. Ord v => v -> Bool -> OBDD v
unit v
v Bool
True