BDD.hs

-- | Core BDD types.
module Imp.BDD
  ( VarLabel(..)
  , NodeId(..)
  , BDD(..)
  , BDDNode(..)
  ) where

-- | A BDD variable label (index into the variable ordering).
newtype VarLabel = VarLabel { unVarLabel :: Int }
  deriving newtype (Eq, Ord, Show)

-- | A BDD node ID (index into the node table).
newtype NodeId = NodeId { unNodeId :: Int }
  deriving newtype (Eq, Ord, Show)

-- | A BDD pointer with complemented edges for O(1) negation.
data BDD
  = BDDTrue
  | BDDFalse
  | BDDRef  !NodeId   -- ^ positive reference
  | BDDComp !NodeId   -- ^ complemented reference
  deriving stock (Eq, Ord, Show)

-- | Internal BDD node: variable, low child, and high child.
data BDDNode = BDDNode
  { bddVar  :: !VarLabel
  , bddLow  :: !BDD
  , bddHigh :: !BDD
  } deriving stock (Eq, Ord, Show)