add isSubsetOf, isProperSubsetOf, and disjoint to ZDD

src/Data/DecisionDiagram/ZDD.hs

@@ -40,6 +40,9 @@ module Data.DecisionDiagram.ZDD
   -- * Query
   , null
   , size
+  , isSubsetOf
+  , isProperSubsetOf
+  , disjoint
 
   -- * Combine
   , union
@@ -270,6 +273,18 @@ size (ZDD node) = runST $ do
             return ret
   f node
 
+-- | Is this the empty set?
+isSubsetOf :: ItemOrder a => ZDD a -> ZDD a -> Bool
+isSubsetOf a b = union a b == b
+
+-- | @(s1 `isProperSubsetOf` s2)@ indicates whether @s1@ is a proper subset of @s2@.
+isProperSubsetOf :: ItemOrder a => ZDD a -> ZDD a -> Bool
+isProperSubsetOf a b = a `isSubsetOf` b && a /= b
+
+-- | Check whether two sets are disjoint (i.e., their intersection is empty).
+disjoint :: ItemOrder a => ZDD a -> ZDD a -> Bool
+disjoint a b = null (a `intersection` b)
+
 -- | Convert the family to a set of 'IntSet'.
 toSetOfIntSets :: ZDD a -> Set IntSet
 toSetOfIntSets (ZDD node) = runST $ do

test/TestZDD.hs

@@ -202,6 +202,36 @@ prop_null_size =
     forAll arbitrary $ \(a :: ZDD o) ->
       ZDD.null a === (ZDD.size a == (0 :: Int))
 
+prop_isSubsetOf_refl :: Property
+prop_isSubsetOf_refl =
+  withDefaultOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(a :: ZDD o) ->
+      a `ZDD.isSubsetOf` a
+
+prop_isSubsetOf_empty :: Property
+prop_isSubsetOf_empty =
+  withDefaultOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(a :: ZDD o) ->
+      ZDD.empty `ZDD.isSubsetOf` a
+
+prop_isSubsetOf_and_isProperSubsetOf :: Property
+prop_isSubsetOf_and_isProperSubsetOf =
+  withDefaultOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(a :: ZDD o, b) ->
+      (a `ZDD.isSubsetOf` b) === (a `ZDD.isProperSubsetOf` b || a == b)
+
+prop_isProperSubsetOf_not_refl :: Property
+prop_isProperSubsetOf_not_refl =
+  withDefaultOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(a :: ZDD o) ->
+      not (ZDD.isProperSubsetOf a a)
+
+prop_disjoint :: Property
+prop_disjoint =
+  withDefaultOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(a :: ZDD o, b) ->
+      ZDD.disjoint a b === ZDD.null (a `ZDD.intersection` b)
+
 -- ------------------------------------------------------------------------
 
 zddTestGroup :: TestTree