add BDD.ite

src/Data/DecisionDiagram/BDD.hs

@@ -46,6 +46,7 @@ module Data.DecisionDiagram.BDD
   , xor
   , (.=>.)
   , (.<=>.)
+  , ite
   , andB
   , orB
 
@@ -252,6 +253,30 @@ xor = apply' True f
     f a b | a == b = Just T
     f _ _ = Nothing
 
+-- | If-then-else
+ite :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a -> BDD a
+ite c' t' e' = runST $ do
+  h <- C.newSized defaultTableSize
+  let f T t _ = return t
+      f F _ e = return e
+      f _ t e | t == e = return t
+      f c t e = do
+        case minimum [level c, level t, level e] of
+          Terminal -> error "should not happen"
+          NonTerminal x -> do
+            let key = (c, t, e)
+            m <- H.lookup h key
+            case m of
+              Just y -> return y
+              Nothing -> do
+                let (c0, c1) = case c of{ Branch x' lo hi | x' == x -> (lo, hi); _ -> (c, c) }
+                    (t0, t1) = case t of{ Branch x' lo hi | x' == x -> (lo, hi); _ -> (t, t) }
+                    (e0, e1) = case e of{ Branch x' lo hi | x' == x -> (lo, hi); _ -> (e, e) }
+                ret <- liftM2 (Branch x) (f c0 t0 e0) (f c1 t1 e1)
+                H.insert h key ret
+                return ret
+  f c' t' e'
+
 -- | Conjunction of a list of BDDs.
 andB :: forall f a. (Foldable f, ItemOrder a) => f (BDD a) -> BDD a
 andB xs = Foldable.foldl' (.&&.) true xs

test/TestBDD.hs

@@ -268,6 +268,40 @@ prop_equiv =
     forAll arbitrary $ \(a :: BDD o, b) ->
       (a BDD..<=>. b) === ((a BDD..=>. b) BDD..&&. (b BDD..=>. a))
 
+-- ------------------------------------------------------------------------
+-- If-then-else
+-- ------------------------------------------------------------------------
+
+prop_ite :: Property
+prop_ite =
+  withDefaultOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(c :: BDD o, t, e) ->
+      BDD.ite c t e === ((c BDD..&&. t) BDD..||. (BDD.notB c BDD..&&. e))
+
+prop_ite_swap_branch :: Property
+prop_ite_swap_branch =
+  withDefaultOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(c :: BDD o, t, e) ->
+      BDD.ite c t e === BDD.ite (BDD.notB c) e t
+
+prop_ite_dist_not :: Property
+prop_ite_dist_not =
+  withDefaultOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(c :: BDD o, t, e) ->
+      BDD.notB (BDD.ite c t e) === BDD.ite c (BDD.notB t) (BDD.notB e)
+
+prop_ite_dist_and :: Property
+prop_ite_dist_and =
+  withDefaultOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(c :: BDD o, t, e, d) ->
+      (d BDD..&&. BDD.ite c t e) === BDD.ite c (d BDD..&&. t) (d BDD..&&. e)
+
+prop_ite_dist_or :: Property
+prop_ite_dist_or =
+  withDefaultOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(c :: BDD o, t, e, d) ->
+      (d BDD..||. BDD.ite c t e) === BDD.ite c (d BDD..||. t) (d BDD..||. e)
+
 -- ------------------------------------------------------------------------
 -- Quantification
 -- ------------------------------------------------------------------------