decision-diagrams (empty) → 0.1.0.0
raw patch · 13 files changed
+3489/−0 lines, 13 filesdep +QuickCheckdep +basedep +containerssetup-changed
Dependencies added: QuickCheck, base, containers, decision-diagrams, hashable, hashtables, intern, mwc-random, primitive, random, reflection, statistics, tasty, tasty-hunit, tasty-quickcheck, tasty-th, unordered-containers
Files
- ChangeLog.md +3/−0
- LICENSE +29/−0
- README.md +8/−0
- Setup.hs +2/−0
- decision-diagrams.cabal +72/−0
- src/Data/DecisionDiagram/BDD.hs +791/−0
- src/Data/DecisionDiagram/BDD/Internal/ItemOrder.hs +81/−0
- src/Data/DecisionDiagram/BDD/Internal/Node.hs +90/−0
- src/Data/DecisionDiagram/ZDD.hs +843/−0
- test/TestBDD.hs +853/−0
- test/TestSuite.hs +12/−0
- test/TestZDD.hs +681/−0
- test/Utils.hs +24/−0
+ ChangeLog.md view
@@ -0,0 +1,3 @@+# Changelog for decision-diagrams++## Unreleased changes
+ LICENSE view
@@ -0,0 +1,29 @@+BSD 3-Clause License++Copyright (c) 2021, Masahiro Sakai+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this+ list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright notice,+ this list of conditions and the following disclaimer in the documentation+ and/or other materials provided with the distribution.++3. Neither the name of the copyright holder nor the names of its+ contributors may be used to endorse or promote products derived from+ this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,8 @@+# decision-diagrams++[](https://github.com/msakai/haskell-decision-diagrams/actions/workflows/build.yaml)+[](https://coveralls.io/r/msakai/haskell-decision-diagrams)++Binary Decision Diagrams (BDD) and Zero-suppressed Binary Decision Diagrams (ZDD) implementation in Haskell.++Hash-consing is implemented using [intern](https://hackage.haskell.org/package/intern) package.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ decision-diagrams.cabal view
@@ -0,0 +1,72 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.34.4.+--+-- see: https://github.com/sol/hpack++name: decision-diagrams+version: 0.1.0.0+synopsis: Binary Decision Diagrams (BDD) and Zero-suppressed Binary Decision Diagrams (ZDD)+description: Please see the README on GitHub at <https://github.com/msakai/haskell-decision-diagrams#readme>+category: Data, Logic+homepage: https://github.com/msakai/haskell-decision-diagrams#readme+bug-reports: https://github.com/msakai/haskell-decision-diagrams/issues+author: Masahiro Sakai+maintainer: masahiro.sakai@gmail.com+copyright: 2021 Masahiro Sakai+license: BSD3+license-file: LICENSE+build-type: Simple+extra-source-files:+ README.md+ ChangeLog.md++source-repository head+ type: git+ location: https://github.com/msakai/haskell-decision-diagrams++library+ exposed-modules:+ Data.DecisionDiagram.BDD+ Data.DecisionDiagram.BDD.Internal.ItemOrder+ Data.DecisionDiagram.ZDD+ other-modules:+ Data.DecisionDiagram.BDD.Internal.Node+ hs-source-dirs:+ src+ build-depends:+ base >=4.7 && <5+ , containers >=0.5.11.0 && <0.7+ , hashable >=1.2.7.0 && <1.4+ , hashtables >=1.2.3.1 && <1.3+ , intern >=0.9.1.2 && <1.0.0.0+ , mwc-random >=0.13.6.0 && <0.16+ , primitive >=0.6.3.0 && <0.8+ , random >=1.1 && <1.3+ , reflection >=2.1.4 && <2.2+ , unordered-containers >=0.2.9.0 && <0.3+ default-language: Haskell2010++test-suite decision-diagrams-test+ type: exitcode-stdio-1.0+ main-is: TestSuite.hs+ other-modules:+ TestBDD+ TestZDD+ Utils+ Paths_decision_diagrams+ hs-source-dirs:+ test+ ghc-options: -threaded -rtsopts -with-rtsopts=-N+ build-depends:+ QuickCheck >=2.11.3 && <2.15+ , base >=4.7 && <5+ , containers >=0.5.11.0 && <0.7+ , decision-diagrams+ , mwc-random >=0.13.6.0 && <0.16+ , statistics >=0.14.0.2 && <0.16+ , tasty >=1.1.0.4 && <1.5+ , tasty-hunit >=0.10.0.1 && <0.11+ , tasty-quickcheck ==0.10.*+ , tasty-th >=0.1.7 && <0.2+ default-language: Haskell2010
+ src/Data/DecisionDiagram/BDD.hs view
@@ -0,0 +1,791 @@+{-# OPTIONS_GHC -Wall #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ViewPatterns #-}+----------------------------------------------------------------------+-- |+-- Module : Data.DecisionDiagram.BDD+-- Copyright : (c) Masahiro Sakai 2021+-- License : BSD-style+--+-- Maintainer : masahiro.sakai@gmail.com+-- Stability : unstable+-- Portability : non-portable+--+-- Reduced Ordered Binary Decision Diagrams (ROBDD).+--+-- References:+--+-- * Bryant, "Graph-Based Algorithms for Boolean Function Manipulation,"+-- in IEEE Transactions on Computers, vol. C-35, no. 8, pp. 677-691,+-- Aug. 1986, doi: [10.1109/TC.1986.1676819](https://doi.org/10.1109/TC.1986.1676819).+-- <https://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf>+--+----------------------------------------------------------------------+module Data.DecisionDiagram.BDD+ (+ -- * The BDD type+ BDD (F, T, Branch)++ -- * Item ordering+ , ItemOrder (..)+ , AscOrder+ , DescOrder+ , withDefaultOrder+ , withAscOrder+ , withDescOrder+ , withCustomOrder++ -- * Boolean operations+ , true+ , false+ , var+ , notB+ , (.&&.)+ , (.||.)+ , xor+ , (.=>.)+ , (.<=>.)+ , ite+ , andB+ , orB++ -- * Quantification+ , forAll+ , exists+ , existsUnique+ , forAllSet+ , existsSet+ , existsUniqueSet++ -- * Query+ , support+ , evaluate++ -- * Restriction / Cofactor+ , restrict+ , restrictSet+ , restrictLaw++ -- * Substition / Composition+ , subst+ , substSet++ -- * Fold+ , fold+ , fold'++ -- * Conversion from/to graphs+ , Graph+ , Node (..)+ , toGraph+ , toGraph'+ , fromGraph+ , fromGraph'+ ) where++import Control.Exception (assert)+import Control.Monad+import Control.Monad.ST+import Data.Function (on)+import Data.Functor.Identity+import Data.Hashable+import qualified Data.HashTable.Class as H+import qualified Data.HashTable.ST.Cuckoo as C+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import Data.IntSet (IntSet)+import qualified Data.IntSet as IntSet+import Data.List (sortBy)+import Data.Proxy+import Data.STRef+import Text.Read++import Data.DecisionDiagram.BDD.Internal.ItemOrder+import qualified Data.DecisionDiagram.BDD.Internal.Node as Node++infixr 3 .&&.+infixr 2 .||.+infixr 1 .=>.+infix 1 .<=>.++-- ------------------------------------------------------------------------++defaultTableSize :: Int+defaultTableSize = 256++-- ------------------------------------------------------------------------++-- | Reduced ordered binary decision diagram representing boolean function+newtype BDD a = BDD Node.Node+ deriving (Eq, Hashable)++pattern F :: BDD a+pattern F = BDD Node.F++pattern T :: BDD a+pattern T = BDD Node.T++-- | Smart constructor that takes the BDD reduction rules into account+pattern Branch :: Int -> BDD a -> BDD a -> BDD a+pattern Branch x lo hi <- BDD (Node.Branch x (BDD -> lo) (BDD -> hi)) where+ Branch x (BDD lo) (BDD hi)+ | lo == hi = BDD lo+ | otherwise = BDD (Node.Branch x lo hi)++{-# COMPLETE T, F, Branch #-}++nodeId :: BDD a -> Int+nodeId (BDD node) = Node.nodeId node++data BDDCase2 a+ = BDDCase2LT Int (BDD a) (BDD a)+ | BDDCase2GT Int (BDD a) (BDD a)+ | BDDCase2EQ Int (BDD a) (BDD a) (BDD a) (BDD a)+ | BDDCase2EQ2 Bool Bool++bddCase2 :: forall a. ItemOrder a => Proxy a -> BDD a -> BDD a -> BDDCase2 a+bddCase2 _ (Branch ptop p0 p1) (Branch qtop q0 q1) =+ case compareItem (Proxy :: Proxy a) ptop qtop of+ LT -> BDDCase2LT ptop p0 p1+ GT -> BDDCase2GT qtop q0 q1+ EQ -> BDDCase2EQ ptop p0 p1 q0 q1+bddCase2 _ (Branch ptop p0 p1) _ = BDDCase2LT ptop p0 p1+bddCase2 _ _ (Branch qtop q0 q1) = BDDCase2GT qtop q0 q1+bddCase2 _ T T = BDDCase2EQ2 True True+bddCase2 _ T F = BDDCase2EQ2 True False+bddCase2 _ F T = BDDCase2EQ2 False True+bddCase2 _ F F = BDDCase2EQ2 False False++level :: BDD a -> Level a+level T = Terminal+level F = Terminal+level (Branch x _ _) = NonTerminal x++-- ------------------------------------------------------------------------++instance Show (BDD a) where+ showsPrec d a = showParen (d > 10) $+ showString "fromGraph " . shows (toGraph a)++instance Read (BDD a) where+ readPrec = parens $ prec 10 $ do+ Ident "fromGraph" <- lexP+ gv <- readPrec+ return (fromGraph gv)++ readListPrec = readListPrecDefault++-- ------------------------------------------------------------------------++-- | True+true :: BDD a+true = T++-- | False+false :: BDD a+false = F++-- | A variable \(x_i\)+var :: Int -> BDD a+var ind = Branch ind F T++-- | Negation of a boolean function+notB :: BDD a -> BDD a+notB bdd = runST $ do+ h <- C.newSized defaultTableSize+ let f T = return F+ f F = return T+ f n@(Branch ind lo hi) = do+ m <- H.lookup h n+ case m of+ Just y -> return y+ Nothing -> do+ ret <- liftM2 (Branch ind) (f lo) (f hi)+ H.insert h n ret+ return ret+ f bdd++apply :: forall a. ItemOrder a => Bool -> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a+apply isCommutative func bdd1 bdd2 = runST $ do+ op <- mkApplyOp isCommutative func+ op bdd1 bdd2++mkApplyOp :: forall a s. ItemOrder a => Bool -> (BDD a -> BDD a -> Maybe (BDD a)) -> ST s (BDD a -> BDD a -> ST s (BDD a))+mkApplyOp isCommutative func = do+ h <- C.newSized defaultTableSize+ let f a b | Just c <- func a b = return c+ f n1 n2 = do+ let key = if isCommutative && nodeId n2 < nodeId n1 then (n2, n1) else (n1, n2)+ m <- H.lookup h key+ case m of+ Just y -> return y+ Nothing -> do+ ret <- case bddCase2 (Proxy :: Proxy a) n1 n2 of+ BDDCase2GT x2 lo2 hi2 -> liftM2 (Branch x2) (f n1 lo2) (f n1 hi2)+ BDDCase2LT x1 lo1 hi1 -> liftM2 (Branch x1) (f lo1 n2) (f hi1 n2)+ BDDCase2EQ x lo1 hi1 lo2 hi2 -> liftM2 (Branch x) (f lo1 lo2) (f hi1 hi2)+ BDDCase2EQ2 _ _ -> error "apply: should not happen"+ H.insert h key ret+ return ret+ return f++-- | Conjunction of two boolean function+(.&&.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a+(.&&.) bdd1 bdd2 = runST $ do+ op <- mkAndOp+ op bdd1 bdd2++mkAndOp :: forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))+mkAndOp = mkApplyOp True f+ where+ f T b = Just b+ f F _ = Just F+ f a T = Just a+ f _ F = Just F+ f a b | a == b = Just a+ f _ _ = Nothing++-- | Disjunction of two boolean function+(.||.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a+(.||.) bdd1 bdd2 = runST $ do+ op <- mkOrOp+ op bdd1 bdd2++mkOrOp :: forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))+mkOrOp = mkApplyOp True f+ where+ f T _ = Just T+ f F b = Just b+ f _ T = Just T+ f a F = Just a+ f a b | a == b = Just a+ f _ _ = Nothing++-- | XOR+xor :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a+xor bdd1 bdd2 = runST $ do+ op <- mkXOROp+ op bdd1 bdd2++mkXOROp :: forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))+mkXOROp = mkApplyOp True f+ where+ f F b = Just b+ f a F = Just a+ f a b | a == b = Just F+ f _ _ = Nothing++-- | Implication+(.=>.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a+(.=>.) = apply False f+ where+ f F _ = Just T+ f T b = Just b+ f _ T = Just T+ f a b | a == b = Just T+ f _ _ = Nothing++-- | Equivalence+(.<=>.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a+(.<=>.) = apply True f+ where+ f T T = Just T+ f T F = Just F+ f F T = Just F+ f F F = Just T+ 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 = runST $ do+ op <- mkAndOp+ foldM op true xs++-- | Disjunction of a list of BDDs.+orB :: forall f a. (Foldable f, ItemOrder a) => f (BDD a) -> BDD a+orB xs = runST $ do+ op <- mkOrOp+ foldM op false xs++-- ------------------------------------------------------------------------++-- | Universal quantification (∀)+forAll :: forall a. ItemOrder a => Int -> BDD a -> BDD a+forAll x bdd = runST $ do+ andOp <- mkAndOp+ h <- C.newSized defaultTableSize+ let f n@(Branch ind lo hi) = do+ m <- H.lookup h n+ case m of+ Just y -> return y+ Nothing -> do+ ret <- if ind == x+ then andOp lo hi+ else liftM2 (Branch ind) (f lo) (f hi)+ H.insert h n ret+ return ret+ f a = return a+ f bdd++-- | Existential quantification (∃)+exists :: forall a. ItemOrder a => Int -> BDD a -> BDD a+exists x bdd = runST $ do+ orOp <- mkOrOp+ h <- C.newSized defaultTableSize+ let f n@(Branch ind lo hi) = do+ m <- H.lookup h n+ case m of+ Just y -> return y+ Nothing -> do+ ret <- if ind == x+ then orOp lo hi+ else liftM2 (Branch ind) (f lo) (f hi)+ H.insert h n ret+ return ret+ f a = return a+ f bdd++-- | Unique existential quantification (∃!)+existsUnique :: forall a. ItemOrder a => Int -> BDD a -> BDD a+existsUnique x bdd = runST $ do+ xorOp <- mkXOROp+ h <- C.newSized defaultTableSize+ let f n@(Branch ind lo hi) = do+ m <- H.lookup h n+ case m of+ Just y -> return y+ Nothing -> do+ ret <- case compareItem (Proxy :: Proxy a) ind x of+ LT -> liftM2 (Branch ind) (f lo) (f hi)+ EQ -> xorOp lo hi+ GT -> return F+ H.insert h n ret+ return ret+ f _ = return F+ f bdd++-- | Universal quantification (∀) over a set of variables+forAllSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a+forAllSet vars bdd = runST $ do+ andOp <- mkAndOp+ h <- C.newSized defaultTableSize+ let f xxs@(x : xs) n@(Branch ind lo hi) = do+ m <- H.lookup h n+ case m of+ Just y -> return y+ Nothing -> do+ ret <- case compareItem (Proxy :: Proxy a) ind x of+ LT -> liftM2 (Branch ind) (f xxs lo) (f xxs hi)+ EQ -> do+ r0 <- f xs lo+ r1 <- f xs hi+ andOp r0 r1+ GT -> f xs n+ H.insert h n ret+ return ret+ f _ a = return a+ f (sortBy (compareItem (Proxy :: Proxy a)) (IntSet.toList vars)) bdd++-- | Existential quantification (∃) over a set of variables+existsSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a+existsSet vars bdd = runST $ do+ orOp <- mkOrOp+ h <- C.newSized defaultTableSize+ let f xxs@(x : xs) n@(Branch ind lo hi) = do+ m <- H.lookup h n+ case m of+ Just y -> return y+ Nothing -> do+ ret <- case compareItem (Proxy :: Proxy a) ind x of+ LT -> liftM2 (Branch ind) (f xxs lo) (f xxs hi)+ EQ -> do+ r0 <- f xs lo+ r1 <- f xs hi+ orOp r0 r1+ GT -> f xs n+ H.insert h n ret+ return ret+ f _ a = return a+ f (sortBy (compareItem (Proxy :: Proxy a)) (IntSet.toList vars)) bdd++-- | Unique existential quantification (∃!) over a set of variables+existsUniqueSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a+existsUniqueSet vars bdd = runST $ do+ xorOp <- mkXOROp+ h <- C.newSized defaultTableSize+ let f xxs@(x : xs) n@(Branch ind lo hi) = do+ let key = (xxs, n)+ m <- H.lookup h key+ case m of+ Just y -> return y+ Nothing -> do+ ret <- case compareItem (Proxy :: Proxy a) ind x of+ LT -> liftM2 (Branch ind) (f xxs lo) (f xxs hi)+ EQ -> do+ r0 <- f xs lo+ r1 <- f xs hi+ xorOp r0 r1+ GT -> return F+ H.insert h key ret+ return ret+ f (_ : _) _ = return F+ f [] a = return a+ f (sortBy (compareItem (Proxy :: Proxy a)) (IntSet.toList vars)) bdd++-- ------------------------------------------------------------------------++-- | Fold over the graph structure of the BDD.+--+-- It takes values for substituting 'false' ('F') and 'true' ('T'),+-- and a function for substiting non-terminal node ('Branch').+fold :: b -> b -> (Int -> b -> b -> b) -> BDD a -> b+fold ff tt br bdd = runST $ do+ h <- C.newSized defaultTableSize+ let f F = return ff+ f T = return tt+ f p@(Branch top lo hi) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ r0 <- f lo+ r1 <- f hi+ let ret = br top r0 r1+ H.insert h p ret+ return ret+ f bdd++-- | Strict version of 'fold'+fold' :: b -> b -> (Int -> b -> b -> b) -> BDD a -> b+fold' ff tt br bdd = runST $ do+ op <- mkFold'Op ff tt br+ op bdd++mkFold'Op :: b -> b -> (Int -> b -> b -> b) -> ST s (BDD a -> ST s b)+mkFold'Op !ff !tt br = do+ h <- C.newSized defaultTableSize+ let f F = return ff+ f T = return tt+ f p@(Branch top lo hi) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ r0 <- f lo+ r1 <- f hi+ let ret = br top r0 r1+ seq ret $ H.insert h p ret+ return ret+ return f++-- ------------------------------------------------------------------------++-- | All the variables that this BDD depends on.+support :: BDD a -> IntSet+support bdd = runST $ do+ op <- mkSupportOp+ op bdd++mkSupportOp :: ST s (BDD a -> ST s IntSet)+mkSupportOp = mkFold'Op IntSet.empty IntSet.empty f+ where+ f x lo hi = IntSet.insert x (lo `IntSet.union` hi)++-- | Evaluate a boolean function represented as BDD under the valuation+-- given by @(Int -> Bool)@, i.e. it lifts a valuation function from+-- variables to BDDs.+evaluate :: (Int -> Bool) -> BDD a -> Bool+evaluate f = g+ where+ g F = False+ g T = True+ g (Branch x lo hi)+ | f x = g hi+ | otherwise = g lo++-- ------------------------------------------------------------------------++-- | Compute \(F_x \) or \(F_{\neg x} \).+restrict :: forall a. ItemOrder a => Int -> Bool -> BDD a -> BDD a+restrict x val bdd = runST $ do+ h <- C.newSized defaultTableSize+ let f T = return T+ f F = return F+ f n@(Branch ind lo hi) = do+ m <- H.lookup h n+ case m of+ Just y -> return y+ Nothing -> do+ ret <- case compareItem (Proxy :: Proxy a) ind x of+ GT -> return n+ LT -> liftM2 (Branch ind) (f lo) (f hi)+ EQ -> if val then return hi else return lo+ H.insert h n ret+ return ret+ f bdd++-- | Compute \(F_{\{x_i = v_i\}_i} \).+restrictSet :: forall a. ItemOrder a => IntMap Bool -> BDD a -> BDD a+restrictSet val bdd = runST $ do+ h <- C.newSized defaultTableSize+ let f [] n = return n+ f _ T = return T+ f _ F = return F+ f xxs@((x,v) : xs) n@(Branch ind lo hi) = do+ m <- H.lookup h n+ case m of+ Just y -> return y+ Nothing -> do+ ret <- case compareItem (Proxy :: Proxy a) ind x of+ GT -> f xs n+ LT -> liftM2 (Branch ind) (f xxs lo) (f xxs hi)+ EQ -> if v then f xs hi else f xs lo+ H.insert h n ret+ return ret+ f (sortBy (compareItem (Proxy :: Proxy a) `on` fst) (IntMap.toList val)) bdd++-- | Compute generalized cofactor of F with respect to C.+--+-- Note that C is the first argument.+restrictLaw :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a+restrictLaw law bdd = runST $ do+ h <- C.newSized defaultTableSize+ let f T n = return n+ f F _ = return T -- Is this correct?+ f _ F = return F+ f _ T = return T+ f n1 n2 | n1 == n2 = return T+ f n1 n2 = do+ m <- H.lookup h (n1, n2)+ case m of+ Just y -> return y+ Nothing -> do+ ret <- case bddCase2 (Proxy :: Proxy a) n1 n2 of+ BDDCase2GT x2 lo2 hi2 -> liftM2 (Branch x2) (f n1 lo2) (f n1 hi2)+ BDDCase2EQ x1 lo1 hi1 lo2 hi2+ | lo1 == F -> f hi1 hi2+ | hi1 == F -> f lo1 lo2+ | otherwise -> liftM2 (Branch x1) (f lo1 lo2) (f hi1 hi2)+ BDDCase2LT x1 lo1 hi1+ | lo1 == F -> f hi1 n2+ | hi1 == F -> f lo1 n2+ | otherwise -> liftM2 (Branch x1) (f lo1 n2) (f hi1 n2)+ BDDCase2EQ2 _ _ -> error "restrictLaw: should not happen"+ H.insert h (n1, n2) ret+ return ret+ f law bdd++-- ------------------------------------------------------------------------++-- | @subst x N M@ computes substitution \(M_{x = N}\).+--+-- This operation is also known as /Composition/.+subst :: forall a. ItemOrder a => Int -> BDD a -> BDD a -> BDD a+subst x n m = runST $ do+ h <- C.newSized defaultTableSize+ let f (Branch x' lo _) mhi n2 | x==x' = f lo mhi n2+ f mlo (Branch x' _ hi) n2 | x==x' = f mlo hi n2+ f mlo _ F = return $ restrict x False mlo+ f _ mhi T = return $ restrict x True mhi+ f mlo mhi n2 = do+ u <- H.lookup h (mlo, mhi, n2)+ case u of+ Just y -> return y+ Nothing -> do+ case minimum (map level [mlo, mhi, n2]) of+ Terminal -> error "should not happen"+ NonTerminal x' -> do+ let (mll, mlh) =+ case mlo of+ Branch x'' mll' mlh' | x' == x'' -> (mll', mlh')+ _ -> (mlo, mlo)+ (mhl, mhh) =+ case mhi of+ Branch x'' mhl' mhh' | x' == x'' -> (mhl', mhh')+ _ -> (mhi, mhi)+ (n2l, n2h) =+ case n2 of+ Branch x'' n2l' n2h' | x' == x'' -> (n2l', n2h')+ _ -> (n2, n2)+ r0 <- f mll mhl n2l+ r1 <- f mlh mhh n2h+ let ret = Branch x' r0 r1+ H.insert h (mlo, mhi, n2) ret+ return ret+ f m m n++-- | Simultaneous substitution+substSet :: forall a. ItemOrder a => IntMap (BDD a) -> BDD a -> BDD a+substSet s m = runST $ do+ supportOp <- mkSupportOp++ h <- C.newSized defaultTableSize+ let -- f :: IntMap (BDD a) -> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST _ (BDD a)+ f conditions conditioned _ | assert (length conditioned >= 1 && all (\(cond, _) -> IntMap.keysSet cond `IntSet.isSubsetOf` IntMap.keysSet conditions) conditioned) False = undefined+ f conditions conditioned remaining = do+ let l1 = minimum $ map (level . snd) conditioned+ -- remaining' = IntMap.filterWithKey (\x _ -> l1 <= NonTerminal x) remaining+ remaining' <- do+ tmp <- liftM IntSet.unions $ mapM (supportOp . snd) conditioned+ return $ IntMap.restrictKeys remaining tmp+ let l = minimum $ l1 : map level (IntMap.elems remaining' ++ IntMap.elems conditions)+ assert (all (\c -> NonTerminal c <= l) (IntMap.keys conditions)) $ return ()+ case l of+ Terminal -> do+ case propagateFixed conditions conditioned of+ (conditions', conditioned') ->+ assert (IntMap.null conditions' && length conditioned' == 1) $+ return (snd (head conditioned'))+ NonTerminal x+ | l == l1 && x `IntMap.member` remaining' -> do+ let conditions' = IntMap.insert x (remaining' IntMap.! x) conditions+ conditioned' = do+ (cond, a) <- conditioned+ case a of+ Branch x' lo hi | x == x' -> [(IntMap.insert x False cond, lo), (IntMap.insert x True cond, hi)]+ _ -> [(cond, a)]+ f conditions' conditioned' (IntMap.delete x remaining')+ | otherwise -> do+ case propagateFixed conditions conditioned of+ (conditions', conditioned') -> do+ let key = (IntMap.toList conditions', [(IntMap.toList cond, a) | (cond, a) <- conditioned'], IntMap.toList remaining') -- キーを減らせる?+ u <- H.lookup h key+ case u of+ Just y -> return y+ Nothing -> do+ let f0 (Branch x' lo _) | x == x' = lo+ f0 a = a+ f1 (Branch x' _ hi) | x == x' = hi+ f1 a = a+ r0 <- f (IntMap.map f0 conditions') [(cond, f0 a) | (cond, a) <- conditioned'] (IntMap.map f0 remaining')+ r1 <- f (IntMap.map f1 conditions') [(cond, f1 a) | (cond, a) <- conditioned'] (IntMap.map f1 remaining')+ let ret = Branch x r0 r1+ H.insert h key ret+ return ret+ f IntMap.empty [(IntMap.empty, m)] s++ where+ propagateFixed :: IntMap (BDD a) -> [(IntMap Bool, BDD a)] -> (IntMap (BDD a), [(IntMap Bool, BDD a)])+ propagateFixed conditions conditioned+ | IntMap.null fixed = (conditions, conditioned)+ | otherwise =+ ( IntMap.difference conditions fixed+ , [(IntMap.difference cond fixed, a) | (cond, a) <- conditioned, and $ IntMap.intersectionWith (==) fixed cond]+ )+ where+ fixed = IntMap.mapMaybe asBool conditions++ asBool :: BDD a -> Maybe Bool+ asBool a =+ case a of+ T -> Just True+ F -> Just False+ _ -> Nothing++-- ------------------------------------------------------------------------++type Graph = IntMap Node++data Node+ = NodeF+ | NodeT+ | NodeBranch !Int Int Int+ deriving (Eq, Show, Read)++-- | Convert a BDD into a pointed graph+toGraph :: BDD a -> (Graph, Int)+toGraph bdd =+ case toGraph' (Identity bdd) of+ (g, Identity v) -> (g, v)++-- | Convert multiple BDDs into a graph+toGraph' :: Traversable t => t (BDD a) -> (Graph, t Int)+toGraph' bs = runST $ do+ h <- C.newSized defaultTableSize+ H.insert h F 0+ H.insert h T 1+ counter <- newSTRef 2+ ref <- newSTRef $ IntMap.fromList [(0, NodeF), (1, NodeT)]++ let f F = return 0+ f T = return 1+ f p@(Branch x lo hi) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ r0 <- f lo+ r1 <- f hi+ n <- readSTRef counter+ writeSTRef counter $! n+1+ H.insert h p n+ modifySTRef' ref (IntMap.insert n (NodeBranch x r0 r1))+ return n++ vs <- mapM f bs+ g <- readSTRef ref+ return (g, vs)++-- | Convert a pointed graph into a BDD+fromGraph :: (Graph, Int) -> BDD a+fromGraph (g, v) =+ case IntMap.lookup v (fromGraph' g) of+ Nothing -> error ("Data.DecisionDiagram.BDD.fromGraph: invalid node id " ++ show v)+ Just bdd -> bdd++-- | Convert nodes of a graph into BDDs+fromGraph' :: Graph -> IntMap (BDD a)+fromGraph' g = ret+ where+ ret = IntMap.map f g+ f NodeF = F+ f NodeT = T+ f (NodeBranch x lo hi) =+ case (IntMap.lookup lo ret, IntMap.lookup hi ret) of+ (Nothing, _) -> error ("Data.DecisionDiagram.BDD.fromGraph': invalid node id " ++ show lo)+ (_, Nothing) -> error ("Data.DecisionDiagram.BDD.fromGraph': invalid node id " ++ show hi)+ (Just lo', Just hi') -> Branch x lo' hi'++-- ------------------------------------------------------------------------++-- https://ja.wikipedia.org/wiki/%E4%BA%8C%E5%88%86%E6%B1%BA%E5%AE%9A%E5%9B%B3+_test_bdd :: BDD AscOrder+_test_bdd = (notB x1 .&&. notB x2 .&&. notB x3) .||. (x1 .&&. x2) .||. (x2 .&&. x3)+ where+ x1 = var 1+ x2 = var 2+ x3 = var 3+{-+BDD (Node 880 (UBranch 1 (Node 611 (UBranch 2 (Node 836 UT) (Node 215 UF))) (Node 806 (UBranch 2 (Node 842 (UBranch 3 (Node 836 UT) (Node 215 UF))) (Node 464 (UBranch 3 (Node 215 UF) (Node 836 UT)))))))+-}++-- ------------------------------------------------------------------------
+ src/Data/DecisionDiagram/BDD/Internal/ItemOrder.hs view
@@ -0,0 +1,81 @@+{-# OPTIONS_GHC -Wall #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}+----------------------------------------------------------------------+-- |+-- Module : Data.DecisionDiagram.BDD.Internal.ItemOrder+-- Copyright : (c) Masahiro Sakai 2021+-- License : BSD-style+--+-- Maintainer : masahiro.sakai@gmail.com+-- Stability : unstable+-- Portability : non-portable+--+----------------------------------------------------------------------+module Data.DecisionDiagram.BDD.Internal.ItemOrder+ (+ -- * Item ordering+ ItemOrder (..)+ , AscOrder+ , DescOrder+ , withDefaultOrder+ , withAscOrder+ , withDescOrder+ , withCustomOrder++ -- * Level+ , Level (..)+ ) where++import Data.Proxy+import Data.Reflection++-- ------------------------------------------------------------------------++class ItemOrder a where+ compareItem :: proxy a -> Int -> Int -> Ordering++data AscOrder++data DescOrder++instance ItemOrder AscOrder where+ compareItem _ = compare++instance ItemOrder DescOrder where+ compareItem _ = flip compare++data CustomOrder a++instance Reifies s (Int -> Int -> Ordering) => ItemOrder (CustomOrder s) where+ compareItem _ = reflect (Proxy :: Proxy s)++withAscOrder :: forall r. (Proxy AscOrder -> r) -> r+withAscOrder k = k Proxy++withDescOrder :: forall r. (Proxy DescOrder -> r) -> r+withDescOrder k = k Proxy++-- | Currently the default order is 'AscOrder'+withDefaultOrder :: forall r. (forall a. ItemOrder a => Proxy a -> r) -> r+withDefaultOrder k = k (Proxy :: Proxy AscOrder)++withCustomOrder :: forall r. (Int -> Int -> Ordering) -> (forall a. ItemOrder a => Proxy a -> r) -> r+withCustomOrder cmp k = reify cmp (\(_ :: Proxy s) -> k (Proxy :: Proxy (CustomOrder s)))++-- ------------------------------------------------------------------------++data Level a+ = NonTerminal !Int+ | Terminal+ deriving (Eq, Show)++instance ItemOrder a => Ord (Level a) where+ compare (NonTerminal x) (NonTerminal y) = compareItem (Proxy :: Proxy a) x y+ compare (NonTerminal _) Terminal = LT+ compare Terminal (NonTerminal _) = GT+ compare Terminal Terminal = EQ++-- ------------------------------------------------------------------------
+ src/Data/DecisionDiagram/BDD/Internal/Node.hs view
@@ -0,0 +1,90 @@+{-# OPTIONS_GHC -Wall #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}+----------------------------------------------------------------------+-- |+-- Module : Data.DecisionDiagram.BDD.Internal.Node+-- Copyright : (c) Masahiro Sakai 2021+-- License : BSD-style+--+-- Maintainer : masahiro.sakai@gmail.com+-- Stability : unstable+-- Portability : non-portable+--+----------------------------------------------------------------------+module Data.DecisionDiagram.BDD.Internal.Node+ (+ -- * Low level node type+ Node (T, F, Branch)+ , nodeId+ ) where++import Data.Hashable+import Data.Interned+import GHC.Generics++-- ------------------------------------------------------------------------++-- | Hash-consed node types in BDD or ZDD+data Node = Node {-# UNPACK #-} !Id UNode+ deriving (Show)++instance Eq Node where+ Node i _ == Node j _ = i == j++instance Hashable Node where+ hashWithSalt s (Node i _) = hashWithSalt s i++pattern T :: Node+pattern T <- (unintern -> UT) where+ T = intern UT++pattern F :: Node+pattern F <- (unintern -> UF) where+ F = intern UF++pattern Branch :: Int -> Node -> Node -> Node+pattern Branch ind lo hi <- (unintern -> UBranch ind lo hi) where+ Branch ind lo hi = intern (UBranch ind lo hi)++{-# COMPLETE T, F, Branch #-}++data UNode+ = UT+ | UF+ | UBranch {-# UNPACK #-} !Int Node Node+ deriving (Show)++instance Interned Node where+ type Uninterned Node = UNode+ data Description Node+ = DT+ | DF+ | DBranch {-# UNPACK #-} !Int {-# UNPACK #-} !Id {-# UNPACK #-} !Id+ deriving (Eq, Generic)+ describe UT = DT+ describe UF = DF+ describe (UBranch x (Node i _) (Node j _)) = DBranch x i j+ identify = Node+ cache = nodeCache++instance Hashable (Description Node)++instance Uninternable Node where+ unintern (Node _ uformula) = uformula++nodeCache :: Cache Node+nodeCache = mkCache+{-# NOINLINE nodeCache #-}++nodeId :: Node -> Id+nodeId (Node id_ _) = id_++-- ------------------------------------------------------------------------
+ src/Data/DecisionDiagram/ZDD.hs view
@@ -0,0 +1,843 @@+{-# OPTIONS_GHC -Wall #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}+----------------------------------------------------------------------+-- |+-- Module : Data.DecisionDiagram.ZDD+-- Copyright : (c) Masahiro Sakai 2021+-- License : BSD-style+--+-- Maintainer : masahiro.sakai@gmail.com+-- Stability : unstable+-- Portability : non-portable+--+-- Zero-Suppressed binary decision diagram.+--+-- References:+--+-- * S. Minato, "Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems,"+-- 30th ACM/IEEE Design Automation Conference, 1993, pp. 272-277,+-- doi: [10.1145/157485.164890](https://doi.org/10.1145/157485.164890).+-- <https://www.researchgate.net/publication/221062015_Zero-Suppressed_BDDs_for_Set_Manipulation_in_Combinatorial_Problems>+--+----------------------------------------------------------------------+module Data.DecisionDiagram.ZDD+ (+ -- * ZDD type+ ZDD (Empty, Base, Branch)++ -- * Item ordering+ , ItemOrder (..)+ , AscOrder+ , DescOrder+ , withDefaultOrder+ , withAscOrder+ , withDescOrder+ , withCustomOrder++ -- * Construction+ , empty+ , base+ , singleton+ , subsets+ , fromListOfIntSets+ , fromSetOfIntSets++ -- * Insertion+ , insert++ -- * Deletion+ , delete++ -- * Query+ , member+ , notMember+ , null+ , size+ , isSubsetOf+ , isProperSubsetOf+ , disjoint++ -- * Combine+ , union+ , unions+ , intersection+ , difference+ , (\\)+ , nonSuperset++ -- * Filter+ , subset1+ , subset0++ -- * Map+ , mapInsert+ , mapDelete+ , change++ -- * Fold+ , fold+ , fold'++ -- * Minimal hitting sets+ , minimalHittingSets+ , minimalHittingSetsToda+ , minimalHittingSetsKnuth+ , minimalHittingSetsImai++ -- * Random sampling+ , uniformM++ -- * Min/Max+ , findMinSum+ , findMaxSum++ -- * Misc+ , flatten++ -- * Conversion+ , toListOfIntSets+ , toSetOfIntSets++ -- ** Conversion from/to graphs+ , Graph+ , Node (..)+ , toGraph+ , toGraph'+ , fromGraph+ , fromGraph'+ ) where++import Prelude hiding (null)++import Control.Monad+#if !MIN_VERSION_mwc_random(0,15,0)+import Control.Monad.Primitive+#endif+import Control.Monad.ST+import Data.Functor.Identity+import Data.Hashable+import Data.HashMap.Lazy (HashMap)+import qualified Data.HashMap.Lazy as HashMap+import qualified Data.HashTable.Class as H+import qualified Data.HashTable.ST.Cuckoo as C+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import Data.IntSet (IntSet)+import qualified Data.IntSet as IntSet+import Data.List (foldl', sortBy)+import Data.Maybe+import Data.Proxy+import Data.Ratio+import Data.Set (Set)+import qualified Data.Set as Set+import Data.STRef+import qualified GHC.Exts as Exts+import Numeric.Natural+#if MIN_VERSION_mwc_random(0,15,0)+import System.Random.Stateful (StatefulGen (..))+#else+import System.Random.MWC (Gen)+#endif+import System.Random.MWC.Distributions (bernoulli)+import Text.Read++import Data.DecisionDiagram.BDD.Internal.ItemOrder+import qualified Data.DecisionDiagram.BDD.Internal.Node as Node+import qualified Data.DecisionDiagram.BDD as BDD++-- ------------------------------------------------------------------------++defaultTableSize :: Int+defaultTableSize = 256++-- ------------------------------------------------------------------------++-- | Zero-suppressed binary decision diagram representing family of sets+newtype ZDD a = ZDD Node.Node+ deriving (Eq, Hashable)++pattern Empty :: ZDD a+pattern Empty = ZDD Node.F++pattern Base :: ZDD a+pattern Base = ZDD Node.T++-- | Smart constructor that takes the ZDD reduction rules into account+pattern Branch :: Int -> ZDD a -> ZDD a -> ZDD a+pattern Branch x lo hi <- ZDD (Node.Branch x (ZDD -> lo) (ZDD -> hi)) where+ Branch _ p0 Empty = p0+ Branch x (ZDD lo) (ZDD hi) = ZDD (Node.Branch x lo hi)++{-# COMPLETE Empty, Base, Branch #-}++nodeId :: ZDD a -> Int+nodeId (ZDD node) = Node.nodeId node++-- ------------------------------------------------------------------------++instance Show (ZDD a) where+ showsPrec d a = showParen (d > 10) $+ showString "fromGraph " . shows (toGraph a)++instance Read (ZDD a) where+ readPrec = parens $ prec 10 $ do+ Ident "fromGraph" <- lexP+ gv <- readPrec+ return (fromGraph gv)++ readListPrec = readListPrecDefault++instance ItemOrder a => Exts.IsList (ZDD a) where+ type Item (ZDD a) = IntSet++ fromList = fromListOfSortedList . map f+ where+ f :: IntSet -> [Int]+ f = sortBy (compareItem (Proxy :: Proxy a)) . IntSet.toList++ toList = fold' [] [IntSet.empty] (\top lo hi -> lo <> map (IntSet.insert top) hi)++-- ------------------------------------------------------------------------++data ZDDCase2 a+ = ZDDCase2LT Int (ZDD a) (ZDD a)+ | ZDDCase2GT Int (ZDD a) (ZDD a)+ | ZDDCase2EQ Int (ZDD a) (ZDD a) (ZDD a) (ZDD a)+ | ZDDCase2EQ2 Bool Bool++zddCase2 :: forall a. ItemOrder a => Proxy a -> ZDD a -> ZDD a -> ZDDCase2 a+zddCase2 _ (Branch ptop p0 p1) (Branch qtop q0 q1) =+ case compareItem (Proxy :: Proxy a) ptop qtop of+ LT -> ZDDCase2LT ptop p0 p1+ GT -> ZDDCase2GT qtop q0 q1+ EQ -> ZDDCase2EQ ptop p0 p1 q0 q1+zddCase2 _ (Branch ptop p0 p1) _ = ZDDCase2LT ptop p0 p1+zddCase2 _ _ (Branch qtop q0 q1) = ZDDCase2GT qtop q0 q1+zddCase2 _ Base Base = ZDDCase2EQ2 True True+zddCase2 _ Base Empty = ZDDCase2EQ2 True False+zddCase2 _ Empty Base = ZDDCase2EQ2 False True+zddCase2 _ Empty Empty = ZDDCase2EQ2 False False++-- | The empty set (∅).+empty :: ZDD a+empty = Empty++-- | The set containing only the empty set ({∅}).+base :: ZDD a+base = Base++-- | Create a ZDD that contains only a given set.+singleton :: forall a. ItemOrder a => IntSet -> ZDD a+singleton xs = insert xs empty++-- | Set of all subsets, i.e. powerset+subsets :: forall a. ItemOrder a => IntSet -> ZDD a+subsets = foldl' f Base . sortBy (flip (compareItem (Proxy :: Proxy a))) . IntSet.toList+ where+ f zdd x = Branch x zdd zdd++-- | Select subsets that contain a particular element and then remove the element from them+subset1 :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a+subset1 var zdd = runST $ do+ h <- C.newSized defaultTableSize+ let f Base = return Empty+ f Empty = return Empty+ f p@(Branch top p0 p1) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ ret <- case compareItem (Proxy :: Proxy a) top var of+ GT -> return Empty+ EQ -> return p1+ LT -> liftM2 (Branch top) (f p0) (f p1)+ H.insert h p ret+ return ret+ f zdd++-- | Subsets that does not contain a particular element+subset0 :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a+subset0 var zdd = runST $ do+ h <- C.newSized defaultTableSize+ let f p@Base = return p+ f Empty = return Empty+ f p@(Branch top p0 p1) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ ret <- case compareItem (Proxy :: Proxy a) top var of+ GT -> return p+ EQ -> return p0+ LT -> liftM2 (Branch top) (f p0) (f p1)+ H.insert h p ret+ return ret+ f zdd++-- | Insert a set into the ZDD.+insert :: forall a. ItemOrder a => IntSet -> ZDD a -> ZDD a+insert xs = f (sortBy (compareItem (Proxy :: Proxy a)) (IntSet.toList xs))+ where+ f [] Empty = Base+ f [] Base = Base+ f [] (Branch top p0 p1) = Branch top (f [] p0) p1+ f (y : ys) Empty = Branch y Empty (f ys Empty)+ f (y : ys) Base = Branch y Base (f ys Empty)+ f yys@(y : ys) p@(Branch top p0 p1) =+ case compareItem (Proxy :: Proxy a) y top of+ LT -> Branch y p (f ys Empty)+ GT -> Branch top (f yys p0) p1+ EQ -> Branch top p0 (f ys p1)++-- | Delete a set from the ZDD.+delete :: forall a. ItemOrder a => IntSet -> ZDD a -> ZDD a+delete xs = f (sortBy (compareItem (Proxy :: Proxy a)) (IntSet.toList xs))+ where+ f [] Empty = Empty+ f [] Base = Empty+ f [] (Branch top p0 p1) = Branch top (f [] p0) p1+ f (_ : _) Empty = Empty+ f (_ : _) Base = Base+ f yys@(y : ys) p@(Branch top p0 p1) =+ case compareItem (Proxy :: Proxy a) y top of+ LT -> p+ GT -> Branch top (f yys p0) p1+ EQ -> Branch top p0 (f ys p1)++-- | Insert an item into each element set of ZDD.+mapInsert :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a+mapInsert var zdd = runST $ do+ unionOp <- mkUnionOp+ h <- C.newSized defaultTableSize+ let f p@Base = return (Branch var Empty p)+ f Empty = return Empty+ f p@(Branch top p0 p1) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ ret <- case compareItem (Proxy :: Proxy a) top var of+ GT -> return (Branch var Empty p)+ LT -> liftM2 (Branch top) (f p0) (f p1)+ EQ -> liftM (Branch top Empty) (unionOp p0 p1)+ H.insert h p ret+ return ret+ f zdd++-- | Delete an item from each element set of ZDD.+mapDelete :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a+mapDelete var zdd = runST $ do+ unionOp <- mkUnionOp+ h <- C.newSized defaultTableSize+ let f Base = return Base+ f Empty = return Empty+ f p@(Branch top p0 p1) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ ret <- case compareItem (Proxy :: Proxy a) top var of+ GT -> return p+ LT -> liftM2 (Branch top) (f p0) (f p1)+ EQ -> unionOp p0 p1+ H.insert h p ret+ return ret+ f zdd++-- | @change x p@ returns {if x∈s then s∖{x} else s∪{x} | s∈P}+change :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a+change var zdd = runST $ do+ h <- C.newSized defaultTableSize+ let f p@Base = return (Branch var Empty p)+ f Empty = return Empty+ f p@(Branch top p0 p1) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ ret <- case compareItem (Proxy :: Proxy a) top var of+ GT -> return (Branch var Empty p)+ EQ -> return (Branch var p1 p0)+ LT -> liftM2 (Branch top) (f p0) (f p1)+ H.insert h p ret+ return ret+ f zdd++-- | Union of two family of sets.+union :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a+union zdd1 zdd2 = runST $ do+ op <- mkUnionOp+ op zdd1 zdd2++mkUnionOp :: forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))+mkUnionOp = do+ h <- C.newSized defaultTableSize+ let f Empty q = return q+ f p Empty = return p+ f p q | p == q = return p+ f p q = do+ let key = if nodeId p <= nodeId q then (p, q) else (q, p)+ m <- H.lookup h key+ case m of+ Just ret -> return ret+ Nothing -> do+ ret <- case zddCase2 (Proxy :: Proxy a) p q of+ ZDDCase2LT ptop p0 p1 -> liftM2 (Branch ptop) (f p0 q) (pure p1)+ ZDDCase2GT qtop q0 q1 -> liftM2 (Branch qtop) (f p q0) (pure q1)+ ZDDCase2EQ top p0 p1 q0 q1 -> liftM2 (Branch top) (f p0 q0) (f p1 q1)+ ZDDCase2EQ2 _ _ -> error "union: should not happen"+ H.insert h key ret+ return ret+ return f++-- | Unions of a list of ZDDs.+unions :: forall f a. (Foldable f, ItemOrder a) => f (ZDD a) -> ZDD a+unions xs = runST $ do+ op <- mkUnionOp+ foldM op empty xs++-- | Intersection of two family of sets.+intersection :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a+intersection zdd1 zdd2 = runST $ do+ op <- mkIntersectionOp+ op zdd1 zdd2++mkIntersectionOp :: forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))+mkIntersectionOp = do+ h <- C.newSized defaultTableSize+ let f Empty _q = return Empty+ f _p Empty = return Empty+ f p q | p == q = return p+ f p q = do+ let key = if nodeId p <= nodeId q then (p, q) else (q, p)+ m <- H.lookup h key+ case m of+ Just ret -> return ret+ Nothing -> do+ ret <- case zddCase2 (Proxy :: Proxy a) p q of+ ZDDCase2LT _ptop p0 _p1 -> f p0 q+ ZDDCase2GT _qtop q0 _q1 -> f p q0+ ZDDCase2EQ top p0 p1 q0 q1 -> liftM2 (Branch top) (f p0 q0) (f p1 q1)+ ZDDCase2EQ2 _ _ -> error "intersection: should not happen"+ H.insert h key ret+ return ret+ return f++-- | Difference of two family of sets.+difference :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a+difference zdd1 zdd2 = runST $ do+ op <- mkDifferenceOp+ op zdd1 zdd2++mkDifferenceOp :: forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))+mkDifferenceOp = do+ h <- C.newSized defaultTableSize+ let f Empty _ = return Empty+ f p Empty = return p+ f p q | p == q = return Empty+ f p q = do+ m <- H.lookup h (p, q)+ case m of+ Just ret -> return ret+ Nothing -> do+ ret <- case zddCase2 (Proxy :: Proxy a) p q of+ ZDDCase2LT ptop p0 p1 -> liftM2 (Branch ptop) (f p0 q) (pure p1)+ ZDDCase2GT _qtop q0 _q1 -> f p q0+ ZDDCase2EQ top p0 p1 q0 q1 -> liftM2 (Branch top) (f p0 q0) (f p1 q1)+ ZDDCase2EQ2 _ _ -> error "difference: should not happen"+ H.insert h (p, q) ret+ return ret+ return f++-- | See 'difference'+(\\) :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a+m1 \\ m2 = difference m1 m2++-- | Given a family P and Q, it computes {S∈P | ∀X∈Q. X⊈S}+--+-- Sometimes it is denoted as /P ↘ Q/.+nonSuperset :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a+nonSuperset zdd1 zdd2 = runST $ do+ op <- mkNonSueprsetOp+ op zdd1 zdd2++mkNonSueprsetOp :: forall a s. ItemOrder a => ST s (ZDD a -> ZDD a -> ST s (ZDD a))+mkNonSueprsetOp = do+ intersectionOp <- mkIntersectionOp + h <- C.newSized defaultTableSize+ let f Empty _ = return Empty+ f _ Base = return Empty+ f p Empty = return p+ f p q | p == q = return Empty+ f p q = do+ m <- H.lookup h (p, q)+ case m of+ Just ret -> return ret+ Nothing -> do+ ret <- case zddCase2 (Proxy :: Proxy a) p q of+ ZDDCase2LT ptop p0 p1 -> liftM2 (Branch ptop) (f p0 q) (f p1 q)+ ZDDCase2GT _qtop q0 _q1 -> f p q0+ ZDDCase2EQ top p0 p1 q0 q1 -> do+ r0 <- f p1 q0+ r1 <- f p1 q1+ liftM2 (Branch top) (f p0 q0) (intersectionOp r0 r1)+ ZDDCase2EQ2 _ _ -> error "nonSuperset: should not happen"+ H.insert h (p, q) ret+ return ret+ return f++minimalHittingSetsKnuth' :: forall a. ItemOrder a => Bool -> ZDD a -> ZDD a+minimalHittingSetsKnuth' imai zdd = runST $ do+ unionOp <- mkUnionOp+ diffOp <- if imai then mkDifferenceOp else mkNonSueprsetOp+ h <- C.newSized defaultTableSize+ let f Empty = return Base+ f Base = return Empty+ f p@(Branch top p0 p1) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ r0 <- f =<< unionOp p0 p1+ r1 <- join $ liftM2 diffOp (f p0) (pure r0)+ let ret = Branch top r0 r1+ H.insert h p ret+ return ret+ f zdd++-- | Minimal hitting sets.+--+-- D. E. Knuth, "The Art of Computer Programming, Volume 4A:+-- Combinatorial Algorithms, Part 1," Addison-Wesley Professional,+-- 2011.+minimalHittingSetsKnuth :: forall a. ItemOrder a => ZDD a -> ZDD a+minimalHittingSetsKnuth = minimalHittingSetsKnuth' False++-- | Minimal hitting sets.+--+-- T. Imai, "One-line hack of knuth's algorithm for minimal hitting set+-- computation with ZDDs," vol. 2015-AL-155, no. 15, Nov. 2015, pp. 1-3.+-- [Online]. Available: <http://id.nii.ac.jp/1001/00145799/>.+minimalHittingSetsImai :: forall a. ItemOrder a => ZDD a -> ZDD a+minimalHittingSetsImai = minimalHittingSetsKnuth' True++-- | Minimal hitting sets.+--+-- * T. Toda, “Hypergraph Transversal Computation with Binary Decision Diagrams,”+-- SEA 2013: Experimental Algorithms.+-- Available: <http://dx.doi.org/10.1007/978-3-642-38527-8_10>.+--+-- * HTC-BDD: Hypergraph Transversal Computation with Binary Decision Diagrams+-- <https://www.disc.lab.uec.ac.jp/toda/htcbdd.html>+minimalHittingSetsToda :: forall a. ItemOrder a => ZDD a -> ZDD a+minimalHittingSetsToda = minimal . hittingSetsBDD++hittingSetsBDD :: forall a. ItemOrder a => ZDD a -> BDD.BDD a+hittingSetsBDD = fold' BDD.true BDD.false (\top h0 h1 -> h0 BDD..&&. BDD.Branch top h1 BDD.true)++minimal :: forall a. ItemOrder a => BDD.BDD a -> ZDD a+minimal bdd = runST $ do+ diffOp <- mkDifferenceOp+ h <- C.newSized defaultTableSize+ let f BDD.F = return Empty+ f BDD.T = return Base+ f p@(BDD.Branch x lo hi) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ ml <- f lo+ mh <- f hi+ ret <- liftM (Branch x ml) (diffOp mh ml)+ H.insert h p ret+ return ret+ f bdd++-- | See 'minimalHittingSetsToda'.+minimalHittingSets :: forall a. ItemOrder a => ZDD a -> ZDD a+minimalHittingSets = minimalHittingSetsToda++-- | Is the set a member of the family?+member :: forall a. (ItemOrder a) => IntSet -> ZDD a -> Bool+member xs = member' xs'+ where+ xs' = sortBy (compareItem (Proxy :: Proxy a)) $ IntSet.toList xs++member' :: forall a. (ItemOrder a) => [Int] -> ZDD a -> Bool+member' [] Base = True+member' [] (Branch _ p0 _) = member' [] p0+member' yys@(y:ys) (Branch top p0 p1) =+ case compareItem (Proxy :: Proxy a) y top of+ EQ -> member' ys p1+ GT -> member' yys p0+ LT -> False+member' _ _ = False++-- | Is the set not in the family?+notMember :: forall a. (ItemOrder a) => IntSet -> ZDD a -> Bool+notMember xs = not . member xs++-- | Is this the empty set?+null :: ZDD a -> Bool+null = (empty ==)++{-# SPECIALIZE size :: ZDD a -> Int #-}+{-# SPECIALIZE size :: ZDD a -> Integer #-}+{-# SPECIALIZE size :: ZDD a -> Natural #-}+-- | The number of sets in the family.+size :: (Integral b) => ZDD a -> b+size = fold' 0 1 (\_ n0 n1 -> n0 + n1)++-- | @(s1 `isSubsetOf` s2)@ indicates whether @s1@ is a subset of @s2@.+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)++--- | Unions of all member sets+flatten :: ItemOrder a => ZDD a -> IntSet+flatten = fold' IntSet.empty IntSet.empty (\top lo hi -> IntSet.insert top (lo `IntSet.union` hi))++-- | Create a ZDD from a set of 'IntSet'+fromSetOfIntSets :: forall a. ItemOrder a => Set IntSet -> ZDD a+fromSetOfIntSets = fromListOfIntSets . Set.toList++-- | Convert the family to a set of 'IntSet'.+toSetOfIntSets :: ZDD a -> Set IntSet+toSetOfIntSets = fold' Set.empty (Set.singleton IntSet.empty) (\top lo hi -> lo <> Set.map (IntSet.insert top) hi)++-- | Create a ZDD from a list of 'IntSet'+fromListOfIntSets :: forall a. ItemOrder a => [IntSet] -> ZDD a+fromListOfIntSets = fromListOfSortedList . map f+ where+ f :: IntSet -> [Int]+ f = sortBy (compareItem (Proxy :: Proxy a)) . IntSet.toList++-- | Convert the family to a list of 'IntSet'.+toListOfIntSets :: ZDD a -> [IntSet]+toListOfIntSets = fold [] [IntSet.empty] (\top lo hi -> lo <> map (IntSet.insert top) hi)++fromListOfSortedList :: forall a. ItemOrder a => [[Int]] -> ZDD a+fromListOfSortedList = unions . map f+ where+ f :: [Int] -> ZDD a+ f = foldr (\x node -> Branch x Empty node) Base++-- | Fold over the graph structure of the ZDD.+--+-- It takes values for substituting 'empty' and 'base',+-- and a function for substiting non-terminal node.+fold :: b -> b -> (Int -> b -> b -> b) -> ZDD a -> b+fold ff tt br zdd = runST $ do+ h <- C.newSized defaultTableSize+ let f Empty = return ff+ f Base = return tt+ f p@(Branch top p0 p1) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ r0 <- f p0+ r1 <- f p1+ let ret = br top r0 r1+ H.insert h p ret+ return ret+ f zdd++-- | Strict version of 'fold'+fold' :: b -> b -> (Int -> b -> b -> b) -> ZDD a -> b+fold' !ff !tt br zdd = runST $ do+ h <- C.newSized defaultTableSize+ let f Empty = return ff+ f Base = return tt+ f p@(Branch top p0 p1) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ r0 <- f p0+ r1 <- f p1+ let ret = br top r0 r1+ seq ret $ H.insert h p ret+ return ret+ f zdd++-- ------------------------------------------------------------------------++-- | Sample a set from uniform distribution over elements of the ZDD.+--+-- The function constructs a table internally and the table is shared across+-- multiple use of the resulting action (@m IntSet@).+-- Therefore, the code+--+-- @+-- let g = uniformM zdd gen+-- s1 <- g+-- s2 <- g+-- @+--+-- is more efficient than+--+-- @+-- s1 <- uniformM zdd gen+-- s2 <- uniformM zdd gen+-- @+-- .+#if MIN_VERSION_mwc_random(0,15,0)+uniformM :: forall a g m. (ItemOrder a, StatefulGen g m) => ZDD a -> g -> m IntSet+#else+uniformM :: forall a m. (ItemOrder a, PrimMonad m) => ZDD a -> Gen (PrimState m) -> m IntSet+#endif+uniformM Empty = error "Data.DecisionDiagram.ZDD.uniformM: empty ZDD"+uniformM zdd = func+ where+ func gen = f zdd []+ where+ f Empty _ = error "Data.DecisionDiagram.ZDD.uniformM: should not happen"+ f Base r = return $ IntSet.fromList r+ f p@(Branch top p0 p1) r = do+ b <- bernoulli (table HashMap.! p) gen+ if b then+ f p1 (top : r)+ else+ f p0 r++ table :: HashMap (ZDD a) Double+ table = runST $ do+ h <- C.newSized defaultTableSize+ let f Empty = return (0 :: Integer)+ f Base = return 1+ f p@(Branch _ p0 p1) = do+ m <- H.lookup h p+ case m of+ Just (ret, _) -> return ret+ Nothing -> do+ n0 <- f p0+ n1 <- f p1+ let s = n0 + n1+ r :: Double+ r = realToFrac (n1 % (n0 + n1))+ seq r $ H.insert h p (s, r)+ return s+ _ <- f zdd+ xs <- H.toList h+ return $ HashMap.fromList [(n, r) | (n, (_, r)) <- xs]++-- ------------------------------------------------------------------------++-- | Find a minimum element set with respect to given weight function+--+-- \[+-- \min_{X\in S} \sum_{x\in X} w(x)+-- \]+findMinSum :: forall a w. (ItemOrder a, Num w, Ord w) => (Int -> w) -> ZDD a -> (w, IntSet)+findMinSum weight =+ fromMaybe (error "Data.DecisionDiagram.ZDD.findMinSum: empty ZDD") .+ fold' Nothing (Just (0, IntSet.empty)) f+ where+ f _ _ Nothing = undefined+ f x z1 (Just (w2, s2)) =+ case z1 of+ Just (w1, _) | w1 <= w2' -> z1+ _ -> seq w2' $ seq s2' $ Just (w2', s2')+ where+ w2' = w2 + weight x+ s2' = IntSet.insert x s2++-- | Find a maximum element set with respect to given weight function+--+-- \[+-- \max_{X\in S} \sum_{x\in X} w(x)+-- \]+findMaxSum :: forall a w. (ItemOrder a, Num w, Ord w) => (Int -> w) -> ZDD a -> (w, IntSet)+findMaxSum weight =+ fromMaybe (error "Data.DecisionDiagram.ZDD.findMinSum: empty ZDD") .+ fold' Nothing (Just (0, IntSet.empty)) f+ where+ f _ _ Nothing = undefined+ f x z1 (Just (w2, s2)) =+ case z1 of+ Just (w1, _) | w1 >= w2' -> z1+ _ -> seq w2' $ seq s2' $ Just (w2', s2')+ where+ w2' = w2 + weight x+ s2' = IntSet.insert x s2++-- ------------------------------------------------------------------------++type Graph = IntMap Node++data Node+ = NodeEmpty+ | NodeBase+ | NodeBranch !Int Int Int+ deriving (Eq, Show, Read)++-- | Convert a ZDD into a pointed graph+toGraph :: ZDD a -> (Graph, Int)+toGraph bdd =+ case toGraph' (Identity bdd) of+ (g, Identity v) -> (g, v)++-- | Convert multiple ZDDs into a graph+toGraph' :: Traversable t => t (ZDD a) -> (Graph, t Int)+toGraph' bs = runST $ do+ h <- C.newSized defaultTableSize+ H.insert h Empty 0+ H.insert h Base 1+ counter <- newSTRef 2+ ref <- newSTRef $ IntMap.fromList [(0, NodeEmpty), (1, NodeBase)]++ let f Empty = return 0+ f Base = return 1+ f p@(Branch x lo hi) = do+ m <- H.lookup h p+ case m of+ Just ret -> return ret+ Nothing -> do+ r0 <- f lo+ r1 <- f hi+ n <- readSTRef counter+ writeSTRef counter $! n+1+ H.insert h p n+ modifySTRef' ref (IntMap.insert n (NodeBranch x r0 r1))+ return n++ vs <- mapM f bs+ g <- readSTRef ref+ return (g, vs)++-- | Convert a pointed graph into a ZDD+fromGraph :: (Graph, Int) -> ZDD a+fromGraph (g, v) =+ case IntMap.lookup v (fromGraph' g) of+ Nothing -> error ("Data.DecisionDiagram.ZDD.fromGraph: invalid node id " ++ show v)+ Just bdd -> bdd++-- | Convert nodes of a graph into ZDDs+fromGraph' :: Graph -> IntMap (ZDD a)+fromGraph' g = ret+ where+ ret = IntMap.map f g+ f NodeEmpty = Empty+ f NodeBase = Base+ f (NodeBranch x lo hi) =+ case (IntMap.lookup lo ret, IntMap.lookup hi ret) of+ (Nothing, _) -> error ("Data.DecisionDiagram.ZDD.fromGraph': invalid node id " ++ show lo)+ (_, Nothing) -> error ("Data.DecisionDiagram.ZDD.fromGraph': invalid node id " ++ show hi)+ (Just lo', Just hi') -> Branch x lo' hi'++-- ------------------------------------------------------------------------
+ test/TestBDD.hs view
@@ -0,0 +1,853 @@+{-# OPTIONS_GHC -Wall -Wno-orphans #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+module TestBDD (bddTestGroup) where++import Control.Monad+import qualified Data.IntMap as IntMap+import Data.IntSet (IntSet)+import qualified Data.IntSet as IntSet+import Data.List+import Data.Proxy+import Test.QuickCheck.Function (apply)+import Test.Tasty+import Test.Tasty.HUnit+import Test.Tasty.QuickCheck+import Test.Tasty.TH++import Data.DecisionDiagram.BDD (BDD (..), ItemOrder (..))+import qualified Data.DecisionDiagram.BDD as BDD++import Utils++-- ------------------------------------------------------------------------++instance BDD.ItemOrder a => Arbitrary (BDD a) where+ arbitrary = arbitraryBDDOver =<< liftM IntSet.fromList arbitrary++ shrink (BDD.F) = []+ shrink (BDD.T) = []+ shrink (BDD.Branch x p0 p1) =+ [p0, p1]+ +++ [ BDD.Branch x p0' p1'+ | (p0', p1') <- shrink (p0, p1), p0' /= p1'+ ]++arbitraryBDDOver :: forall a. BDD.ItemOrder a => IntSet -> Gen (BDD a)+arbitraryBDDOver xs = do+ let f vs n = oneof $+ [ return BDD.true+ , return BDD.false+ ]+ +++ [ do v <- elements vs+ let vs' = dropWhile (\v' -> compareItem (Proxy :: Proxy a) v' v /= GT) vs+ lo <- f vs' (n `div` 2)+ hi <- f vs' (n `div` 2) `suchThat` (/= lo)+ return (BDD.Branch v lo hi)+ | n > 0, not (null vs)+ ]+ sized $ f (sortBy (BDD.compareItem (Proxy :: Proxy a)) $ IntSet.toList xs)++-- ------------------------------------------------------------------------+-- conjunction+-- ------------------------------------------------------------------------++prop_and_unitL :: Property+prop_and_unitL =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (BDD.true BDD..&&. a) === a++prop_and_unitR :: Property+prop_and_unitR =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (a BDD..&&. BDD.true) === a++prop_and_falseL :: Property+prop_and_falseL =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (BDD.false BDD..&&. a) === BDD.false++prop_and_falseR :: Property+prop_and_falseR =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (a BDD..&&. BDD.false) === BDD.false++prop_and_comm :: Property+prop_and_comm =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ (a BDD..&&. b) === (b BDD..&&. a)++prop_and_assoc :: Property+prop_and_assoc =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b, c) ->+ (a BDD..&&. (b BDD..&&. c)) === ((a BDD..&&. b) BDD..&&. c)++prop_and_idempotent :: Property+prop_and_idempotent =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (a BDD..&&. a) === a++-- ------------------------------------------------------------------------+-- disjunction+-- ------------------------------------------------------------------------++prop_or_unitL :: Property+prop_or_unitL =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (BDD.false BDD..||. a) === a++prop_or_unitR :: Property+prop_or_unitR =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (a BDD..||. BDD.false) === a++prop_or_trueL :: Property+prop_or_trueL =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (BDD.true BDD..||. a) === BDD.true++prop_or_trueR :: Property+prop_or_trueR =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (a BDD..||. BDD.true) === BDD.true++prop_or_comm :: Property+prop_or_comm =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ (a BDD..||. b) === (b BDD..||. a)++prop_or_assoc :: Property+prop_or_assoc =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b, c) ->+ (a BDD..||. (b BDD..||. c)) === ((a BDD..||. b) BDD..||. c)++prop_or_idempotent :: Property+prop_or_idempotent =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (a BDD..||. a) === a++-- ------------------------------------------------------------------------+-- xor+-- ------------------------------------------------------------------------++prop_xor_unitL :: Property+prop_xor_unitL =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (BDD.false `BDD.xor` a) === a++prop_xor_unitR :: Property+prop_xor_unitR =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (a `BDD.xor` BDD.false) === a++prop_xor_comm :: Property+prop_xor_comm =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ (a `BDD.xor` b) === (b `BDD.xor` a)++prop_xor_assoc :: Property+prop_xor_assoc =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b, c) ->+ (a `BDD.xor` (b `BDD.xor` c)) === ((a `BDD.xor` b) `BDD.xor` c)++prop_xor_involution :: Property+prop_xor_involution =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (a `BDD.xor` a) === BDD.false++prop_xor_dist :: Property+prop_xor_dist =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b, c) ->+ (a BDD..&&. (b `BDD.xor` c)) === ((a BDD..&&. b) `BDD.xor` (a BDD..&&. c))++-- ------------------------------------------------------------------------+-- distributivity+-- ------------------------------------------------------------------------++prop_dist_1 :: Property+prop_dist_1 =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b, c) ->+ (a BDD..&&. (b BDD..||. c)) === ((a BDD..&&. b) BDD..||. (a BDD..&&. c))++prop_dist_2 :: Property+prop_dist_2 =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b, c) ->+ (a BDD..||. (b BDD..&&. c)) === ((a BDD..||. b) BDD..&&. (a BDD..||. c))++prop_absorption_1 :: Property+prop_absorption_1 =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ (a BDD..&&. (a BDD..||. b)) === a++prop_absorption_2 :: Property+prop_absorption_2 =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ (a BDD..||. (a BDD..&&. b)) === a++-- ------------------------------------------------------------------------+-- negation+-- ------------------------------------------------------------------------++prop_double_negation :: Property+prop_double_negation =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ BDD.notB (BDD.notB a) === a++prop_and_complement :: Property+prop_and_complement =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (a BDD..&&. BDD.notB a) === BDD.false++prop_or_complement :: Property+prop_or_complement =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (a BDD..||. BDD.notB a) === BDD.true++prop_de_morgan_1 :: Property+prop_de_morgan_1 =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ BDD.notB (a BDD..||. b) === (BDD.notB a BDD..&&. BDD.notB b)++prop_de_morgan_2 :: Property+prop_de_morgan_2 =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ BDD.notB (a BDD..&&. b) === (BDD.notB a BDD..||. BDD.notB b)++-- ------------------------------------------------------------------------+-- Implication+-- ------------------------------------------------------------------------++prop_imply :: Property+prop_imply =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ (a BDD..=>. b) === (BDD.notB a BDD..||. b)++prop_imply_currying :: Property+prop_imply_currying =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b, c) ->+ ((a BDD..&&. b) BDD..=>. c) === (a BDD..=>. (b BDD..=>. c))++-- ------------------------------------------------------------------------+-- Equivalence+-- ------------------------------------------------------------------------++prop_equiv :: Property+prop_equiv =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ (a BDD..<=>. b) === ((a BDD..=>. b) BDD..&&. (b BDD..=>. a))++-- ------------------------------------------------------------------------+-- If-then-else+-- ------------------------------------------------------------------------++prop_ite :: Property+prop_ite =+ forAllItemOrder $ \(_ :: 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 =+ forAllItemOrder $ \(_ :: 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 =+ forAllItemOrder $ \(_ :: 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 =+ forAllItemOrder $ \(_ :: 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 =+ forAllItemOrder $ \(_ :: 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+-- ------------------------------------------------------------------------++prop_forAll :: Property+prop_forAll =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(x, a :: BDD o) ->+ BDD.forAll x a === (BDD.restrict x True a BDD..&&. BDD.restrict x False a)++prop_exists :: Property+prop_exists =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(x, a :: BDD o) ->+ BDD.exists x a === (BDD.restrict x True a BDD..||. BDD.restrict x False a)++prop_existsUnique :: Property+prop_existsUnique =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(x, a :: BDD o) ->+ BDD.existsUnique x a === (BDD.restrict x True a `BDD.xor` BDD.restrict x False a)++prop_forAll_support :: Property+prop_forAll_support =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(x, a :: BDD o) ->+ let b = BDD.forAll x a+ xs = BDD.support b+ in counterexample (show (b, xs)) $+ x `IntSet.notMember` xs++prop_exists_support :: Property+prop_exists_support =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(x, a :: BDD o) ->+ let b = BDD.exists x a+ xs = BDD.support b+ in counterexample (show (b, xs)) $+ x `IntSet.notMember` xs++prop_existsUnique_support :: Property+prop_existsUnique_support =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(x, a :: BDD o) ->+ let b = BDD.existsUnique x a+ xs = BDD.support b+ in counterexample (show (b, xs)) $+ x `IntSet.notMember` xs++-- ------------------------------------------------------------------------++prop_forAllSet_empty :: Property+prop_forAllSet_empty =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ BDD.forAllSet IntSet.empty a === a++prop_existsSet_empty :: Property+prop_existsSet_empty =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ BDD.existsSet IntSet.empty a === a++prop_existsUniqueSet_empty :: Property+prop_existsUniqueSet_empty =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ BDD.existsUniqueSet IntSet.empty a === a++prop_forAllSet_singleton :: Property+prop_forAllSet_singleton =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(x, a :: BDD o) ->+ BDD.forAllSet (IntSet.singleton x) a === BDD.forAll x a++prop_existsSet_singleton :: Property+prop_existsSet_singleton =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(x, a :: BDD o) ->+ BDD.existsSet (IntSet.singleton x) a === BDD.exists x a++prop_existsUniqueSet_singleton :: Property+prop_existsUniqueSet_singleton =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(x, a :: BDD o) ->+ BDD.existsUniqueSet (IntSet.singleton x) a === BDD.existsUnique x a++prop_forAllSet_union :: Property+prop_forAllSet_union =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(xs1, xs2, a :: BDD o) ->+ BDD.forAllSet (xs1 `IntSet.union` xs2) a === BDD.forAllSet xs2 (BDD.forAllSet xs1 a)++prop_existsSet_union :: Property+prop_existsSet_union =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(xs1, xs2, a :: BDD o) ->+ BDD.existsSet (xs1 `IntSet.union` xs2) a === BDD.existsSet xs2 (BDD.existsSet xs1 a)++prop_existsUniqueSet_union :: Property+prop_existsUniqueSet_union =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitraryDisjointSets $ \(xs1, xs2) ->+ forAll arbitrary $ \(a :: BDD o) ->+ BDD.existsUniqueSet (xs1 `IntSet.union` xs2) a === BDD.existsUniqueSet xs2 (BDD.existsUniqueSet xs1 a)+ where+ arbitraryDisjointSets = do+ (u, v) <- arbitrary+ return (u `IntSet.intersection` v, u IntSet.\\ v)++-- ------------------------------------------------------------------------++case_support_false :: Assertion+case_support_false = BDD.support BDD.false @?= IntSet.empty++case_support_true :: Assertion+case_support_true = BDD.support BDD.true @?= IntSet.empty++prop_support_var :: Property+prop_support_var =+ forAll arbitrary $ \x ->+ BDD.support (BDD.var x) === IntSet.singleton x++prop_support_not :: Property+prop_support_not =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ let lhs = BDD.support a+ rhs = BDD.support (BDD.notB a)+ in lhs === rhs++prop_support_and :: Property+prop_support_and =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ let lhs = BDD.support (a BDD..&&. b)+ rhs = BDD.support a `IntSet.union` BDD.support b+ in counterexample (show (lhs, rhs)) $ lhs `IntSet.isSubsetOf` rhs++prop_support_or :: Property+prop_support_or =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ let lhs = BDD.support (a BDD..||. b)+ rhs = BDD.support a `IntSet.union` BDD.support b+ in counterexample (show (lhs, rhs)) $ lhs `IntSet.isSubsetOf` rhs++-- ------------------------------------------------------------------------++prop_evaluate_var :: Property+prop_evaluate_var =+ forAll arbitrary $ \(f' :: Fun Int Bool) ->+ let f = apply f'+ in forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \x ->+ BDD.evaluate f (BDD.var x :: BDD o) === f x++prop_evaluate_not :: Property+prop_evaluate_not =+ forAll arbitrary $ \(f' :: Fun Int Bool) ->+ let f = apply f'+ in forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ BDD.evaluate f (BDD.notB a) === not (BDD.evaluate f a)++prop_evaluate_and :: Property+prop_evaluate_and =+ forAll arbitrary $ \(f' :: Fun Int Bool) ->+ let f = apply f'+ in forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ BDD.evaluate f (a BDD..&&. b) === (BDD.evaluate f a && BDD.evaluate f b)++prop_evaluate_or :: Property+prop_evaluate_or =+ forAll arbitrary $ \(f' :: Fun Int Bool) ->+ let f = apply f'+ in forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ BDD.evaluate f (a BDD..||. b) === (BDD.evaluate f a || BDD.evaluate f b)++-- ------------------------------------------------------------------------++prop_restrict :: Property+prop_restrict =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll arbitrary $ \x ->+ let b = (BDD.var x BDD..&&. BDD.restrict x True a) BDD..||.+ (BDD.notB (BDD.var x) BDD..&&. BDD.restrict x False a)+ in a === b++prop_restrict_idempotent :: Property+prop_restrict_idempotent =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll arbitrary $ \(x, val) ->+ let b = BDD.restrict x val a+ c = BDD.restrict x val b+ in counterexample (show (b, c)) $ b === c++prop_restrict_not :: Property+prop_restrict_not =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll arbitrary $ \(x, val) ->+ BDD.restrict x val (BDD.notB a) === BDD.notB (BDD.restrict x val a)++prop_restrict_and :: Property+prop_restrict_and =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ forAll arbitrary $ \(x, val) ->+ BDD.restrict x val (a BDD..&&. b) === (BDD.restrict x val a BDD..&&. BDD.restrict x val b)++prop_restrict_or :: Property+prop_restrict_or =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ forAll arbitrary $ \(x, val) ->+ BDD.restrict x val (a BDD..||. b) === (BDD.restrict x val a BDD..||. BDD.restrict x val b)++prop_restrict_var :: Property+prop_restrict_var =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \x ->+ let a :: BDD o+ a = BDD.var x+ in (BDD.restrict x True a === BDD.true) .&&.+ (BDD.restrict x False a === BDD.false)++prop_restrict_support :: Property+prop_restrict_support =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll arbitrary $ \(x, val) ->+ let b = BDD.restrict x val a+ xs = BDD.support b+ in counterexample (show b) $+ counterexample (show xs) $+ x `IntSet.notMember` xs++-- ------------------------------------------------------------------------++prop_restrictSet_empty :: Property+prop_restrictSet_empty =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ BDD.restrictSet IntMap.empty a === a++prop_restrictSet_singleton :: Property+prop_restrictSet_singleton =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll arbitrary $ \(x, val) ->+ BDD.restrict x val a === BDD.restrictSet (IntMap.singleton x val) a++prop_restrictSet_union :: Property+prop_restrictSet_union =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll arbitrary $ \(val1, val2) ->+ and (IntMap.intersectionWith (==) val1 val2)+ ==>+ (BDD.restrictSet val2 (BDD.restrictSet val1 a) === BDD.restrictSet (val1 `IntMap.union` val2) a)++prop_restrictSet_idempotent :: Property+prop_restrictSet_idempotent =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll arbitrary $ \val ->+ let b = BDD.restrictSet val a+ c = BDD.restrictSet val b+ in counterexample (show (b, c)) $ b === c++prop_restrictSet_not :: Property+prop_restrictSet_not =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll arbitrary $ \val ->+ BDD.restrictSet val (BDD.notB a) === BDD.notB (BDD.restrictSet val a)++prop_restrictSet_and :: Property+prop_restrictSet_and =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ forAll arbitrary $ \val ->+ BDD.restrictSet val (a BDD..&&. b) === (BDD.restrictSet val a BDD..&&. BDD.restrictSet val b)++prop_restrictSet_or :: Property+prop_restrictSet_or =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ forAll arbitrary $ \val ->+ BDD.restrictSet val (a BDD..||. b) === (BDD.restrictSet val a BDD..||. BDD.restrictSet val b)++-- ------------------------------------------------------------------------++prop_restrictLaw :: Property+prop_restrictLaw =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll arbitrary $ \law ->+ (law BDD..&&. BDD.restrictLaw law a) === (law BDD..&&. a)++case_restrictLaw_case_0 :: Assertion+case_restrictLaw_case_0 = (law BDD..&&. BDD.restrictLaw law a) @?= (law BDD..&&. a)+ where+ a, law :: BDD BDD.AscOrder+ a = BDD.Branch 2 BDD.F BDD.T+ law = BDD.Branch 1 (BDD.Branch 2 BDD.T BDD.F) (BDD.Branch 2 BDD.F BDD.T)++prop_restrictLaw_true :: Property+prop_restrictLaw_true =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ BDD.restrictLaw BDD.true a === a++prop_restrictLaw_self :: Property+prop_restrictLaw_self =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (a /= BDD.false) ==> BDD.restrictLaw a a === BDD.true++prop_restrictLaw_not_self :: Property+prop_restrictLaw_not_self =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ (a /= BDD.true) ==> BDD.restrictLaw (BDD.notB a) a === BDD.false++prop_restrictLaw_restrictSet :: Property+prop_restrictLaw_restrictSet =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll arbitrary $ \val ->+ let b = BDD.andB [if v then BDD.var x else BDD.notB (BDD.var x) | (x,v) <- IntMap.toList val]+ in BDD.restrictLaw b a === BDD.restrictSet val a++-- prop_restrictLaw_and_condition :: Property+-- prop_restrictLaw_and_condition =+-- forAllItemOrder $ \(_ :: Proxy o) ->+-- forAll arbitrary $ \(a :: BDD o) ->+-- forAll arbitrary $ \(val1, val2) ->+-- let val = val1 BDD..&&. val2+-- in counterexample (show val) $+-- (val /= BDD.false)+-- ==>+-- (BDD.restrictLaw val a === BDD.restrictLaw val2 (BDD.restrictLaw val1 a))++-- counterexample to the above prop_restrictLaw_and_condition+case_restrictLaw_case_1 :: Assertion+case_restrictLaw_case_1 = do+ -- BDD.restrictLaw val a @?= BDD.restrictLaw val2 (BDD.restrictLaw val1 a)+ BDD.restrictLaw val a @?= BDD.Branch 2 BDD.F BDD.T+ BDD.restrictLaw val2 (BDD.restrictLaw val1 a) @?= BDD.Branch 1 BDD.T (Branch 2 BDD.F BDD.T)+ where+ a :: BDD BDD.AscOrder+ a = Branch 2 BDD.F BDD.T -- x2+ val1 = BDD.Branch 1 BDD.F BDD.T -- x1+ val2 = BDD.Branch 1 (BDD.Branch 2 BDD.F BDD.T) BDD.T -- x1 ∨ x2+ val = val1 BDD..&&. val2 -- x1++prop_restrictLaw_or_condition :: Property+prop_restrictLaw_or_condition =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll arbitrary $ \(val1, val2) ->+ let val = val1 BDD..||. val2+ in counterexample (show val) $+ (val BDD..&&. BDD.restrictLaw val a) === (val1 BDD..&&. BDD.restrictLaw val1 a BDD..||. val2 BDD..&&. BDD.restrictLaw val2 a)++prop_restrictLaw_idempotent :: Property+prop_restrictLaw_idempotent =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll arbitrary $ \val ->+ let b = BDD.restrictLaw val a+ c = BDD.restrictLaw val b+ in counterexample (show (b, c)) $ b === c++prop_restrictLaw_not :: Property+prop_restrictLaw_not =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ forAll (arbitrary `suchThat` (/= BDD.false)) $ \val ->+ BDD.restrictLaw val (BDD.notB a) === BDD.notB (BDD.restrictLaw val a)++prop_restrictLaw_and :: Property+prop_restrictLaw_and =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ forAll (arbitrary `suchThat` (/= BDD.false)) $ \val ->+ BDD.restrictLaw val (a BDD..&&. b) === (BDD.restrictLaw val a BDD..&&. BDD.restrictLaw val b)++prop_restrictLaw_or :: Property+prop_restrictLaw_or =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o, b) ->+ forAll (arbitrary `suchThat` (/= BDD.false)) $ \val ->+ BDD.restrictLaw val (a BDD..||. b) === (BDD.restrictLaw val a BDD..||. BDD.restrictLaw val b)++-- prop_restrictLaw_minimality :: Property+-- prop_restrictLaw_minimality =+-- forAllItemOrder $ \(_ :: Proxy o) ->+-- forAll arbitrary $ \(a :: BDD o) ->+-- forAll arbitrary $ \law ->+-- let b = BDD.restrictLaw law a+-- in counterexample (show b) $+-- ((law BDD..&&. b) === (law BDD..&&. a))+-- .&&.+-- conjoin [counterexample (show b') $ (law BDD..&&. b') =/= (law BDD..&&. a) | b' <- shrink b]++case_restrictLaw_non_minimal_1 :: Assertion+case_restrictLaw_non_minimal_1 = do+ (law BDD..&&. BDD.restrictLaw law a) @?= (law BDD..&&. a)+ BDD.restrictLaw law a @?= b -- should be 'a'?+ where+ law, a :: BDD BDD.AscOrder+ law = BDD.Branch 1 (BDD.Branch 2 BDD.F BDD.T) BDD.T -- x1 ∨ x2+ a = BDD.Branch 2 BDD.T BDD.F -- ¬x2+ b = BDD.Branch 1 BDD.F (BDD.Branch 2 BDD.T BDD.F) -- x1 ∧ ¬x2++case_restrictLaw_non_minimal_2 :: Assertion+case_restrictLaw_non_minimal_2 = do+ (law BDD..&&. BDD.restrictLaw law a) @?= (law BDD..&&. a)+ BDD.restrictLaw law a @?= b -- should be 'a'?+ where+ law, a, b :: BDD BDD.AscOrder+ law = BDD.Branch 1 BDD.T (BDD.Branch 2 BDD.F BDD.T) -- ¬x1 ∨ x2+ a = BDD.Branch 2 BDD.F BDD.T -- x2+ b = BDD.Branch 1 (BDD.Branch 2 BDD.F BDD.T) BDD.T -- x1 ∨ x2++-- ------------------------------------------------------------------------++prop_subst_restrict_constant :: Property+prop_subst_restrict_constant =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(m :: BDD o) ->+ forAll arbitrary $ \x ->+ forAll arbitrary $ \val ->+ BDD.subst x (if val then BDD.true else BDD.false) m === BDD.restrict x val m++prop_subst_restrict :: Property+prop_subst_restrict =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(m :: BDD o) ->+ forAll arbitrary $ \x ->+ forAll arbitrary $ \(n :: BDD o) ->+ BDD.subst x n m === ((n BDD..&&. BDD.restrict x True m) BDD..||. (BDD.notB n BDD..&&. BDD.restrict x False m))++prop_subst_same_var :: Property+prop_subst_same_var =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(m :: BDD o) ->+ forAll arbitrary $ \x ->+ BDD.subst x (BDD.var x) m === m++prop_subst_not_occured :: Property+prop_subst_not_occured =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(m :: BDD o) ->+ forAll (arbitrary `suchThat` (\x -> x `IntSet.notMember` (BDD.support m))) $ \x ->+ forAll arbitrary $ \(n :: BDD o) ->+ BDD.subst x n m === m++-- If x1≠x2 and x1∉FV(M2) then M[x1 ↦ M1][x2 ↦ M2] = M[x2 ↦ M2][x1 ↦ M1[x2 ↦ M2]].+prop_subst_dist :: Property+prop_subst_dist =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(x1, m1) ->+ forAll ((,) <$> (arbitrary `suchThat` (/= x1)) <*> (arbitrary `suchThat` (\m2 -> x1 `IntSet.notMember` BDD.support m2))) $ \(x2, m2) ->+ forAll arbitrary $ \(m :: BDD o) ->+ BDD.subst x2 m2 (BDD.subst x1 m1 m) === BDD.subst x1 (BDD.subst x2 m2 m1) (BDD.subst x2 m2 m)++-- ------------------------------------------------------------------------++prop_substSet_empty :: Property+prop_substSet_empty =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(m :: BDD o) ->+ BDD.substSet IntMap.empty m === m++prop_substSet_singleton :: Property+prop_substSet_singleton =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(m :: BDD o) ->+ forAll arbitrary $ \x ->+ forAll arbitrary $ \m1 ->+ BDD.substSet (IntMap.singleton x m1) m === BDD.subst x m1 m++case_substSet_case_1 :: Assertion+case_substSet_case_1 = do+ BDD.substSet (IntMap.singleton x m1) m @?= BDD.subst x m1 m+ where+ m :: BDD BDD.AscOrder+ m = BDD.Branch 1 (BDD.Branch 2 BDD.T BDD.F) (BDD.Branch 2 BDD.F BDD.F)+ x = 1+ m1 = BDD.Branch 1 BDD.T BDD.F++prop_substSet_same_vars :: Property+prop_substSet_same_vars =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(m :: BDD o) ->+ forAll arbitrary $ \xs ->+ BDD.substSet (IntMap.fromAscList [(x, BDD.var x) | x <- IntSet.toAscList xs]) m === m++prop_substSet_not_occured :: Property+prop_substSet_not_occured =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(m :: BDD o) ->+ forAll (f (BDD.support m)) $ \s ->+ BDD.substSet s m === m+ where+ f xs = liftM IntMap.fromList $ listOf $ do+ y <- arbitrary `suchThat` (`IntSet.notMember` xs)+ m <- arbitrary+ return (y, m)++prop_substSet_compose :: Property+prop_substSet_compose =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll (liftM IntSet.fromList arbitrary) $ \xs ->+ forAll (liftM IntSet.fromList arbitrary) $ \ys ->+ forAll (liftM IntMap.fromList $ mapM (\x -> (,) <$> pure x <*> arbitraryBDDOver ys) (IntSet.toList xs)) $ \s1 ->+ forAll (liftM IntMap.fromList $ mapM (\y -> (,) <$> pure y <*> arbitrary) (IntSet.toList ys)) $ \s2 ->+ forAll (arbitraryBDDOver xs) $ \(m :: BDD o) ->+ BDD.substSet s2 (BDD.substSet s1 m) === BDD.substSet (IntMap.map (BDD.substSet s2) s1) m++case_substSet_case_2 :: Assertion+case_substSet_case_2 = do+ let m :: BDD BDD.AscOrder+ m = BDD.var 1 BDD..&&. BDD.var 2+ BDD.substSet (IntMap.fromList [(1, BDD.var 2), (2, BDD.var 3)]) m @?= BDD.var 2 BDD..&&. BDD.var 3+ BDD.substSet (IntMap.fromList [(1, BDD.var 3), (2, BDD.var 1)]) m @?= BDD.var 3 BDD..&&. BDD.var 1++-- ------------------------------------------------------------------------++prop_toGraph_fromGraph :: Property+prop_toGraph_fromGraph = do+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: BDD o) ->+ BDD.fromGraph (BDD.toGraph a) === a++-- ------------------------------------------------------------------------++bddTestGroup :: TestTree+bddTestGroup = $(testGroupGenerator)
+ test/TestSuite.hs view
@@ -0,0 +1,12 @@+module Main where++import Test.Tasty (defaultMain, testGroup)++import TestBDD+import TestZDD++main :: IO ()+main = defaultMain $ testGroup "decision-diagram test suite"+ [ bddTestGroup+ , zddTestGroup+ ]
+ test/TestZDD.hs view
@@ -0,0 +1,681 @@+{-# OPTIONS_GHC -Wall -Wno-orphans #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+module TestZDD (zddTestGroup) where++import Control.Monad+import Data.IntSet (IntSet)+import qualified Data.IntSet as IntSet+import Data.List+import qualified Data.Map.Strict as Map+import Data.Proxy+import Data.Set (Set)+import qualified Data.Set as Set+import qualified GHC.Exts as Exts+import Statistics.Distribution+import Statistics.Distribution.ChiSquared (chiSquared)+import qualified System.Random.MWC as Rand+import Test.QuickCheck.Function (apply)+import qualified Test.QuickCheck.Monadic as QM+import Test.Tasty+import Test.Tasty.HUnit+import Test.Tasty.QuickCheck+import Test.Tasty.TH++import Data.DecisionDiagram.ZDD (ZDD (..), ItemOrder (..))+import qualified Data.DecisionDiagram.ZDD as ZDD++import Utils++-- ------------------------------------------------------------------------++instance ZDD.ItemOrder a => Arbitrary (ZDD a) where+ arbitrary = do+ vars <- liftM (sortBy (ZDD.compareItem (Proxy :: Proxy a)) . IntSet.toList . IntSet.fromList) arbitrary+ let f vs n = oneof $+ [ return ZDD.empty+ , return ZDD.base+ ]+ +++ [ do v <- elements vs+ let vs' = dropWhile (\v' -> compareItem (Proxy :: Proxy a) v' v /= GT) vs+ p0 <- f vs' (n `div` 2)+ p1 <- f vs' (n `div` 2) `suchThat` (/= ZDD.empty)+ return (ZDD.Branch v p0 p1)+ | n > 0, not (null vs)+ ]+ sized (f vars)++ shrink (ZDD.Empty) = []+ shrink (ZDD.Base) = []+ shrink (ZDD.Branch x p0 p1) =+ [p0, p1]+ +++ [ ZDD.Branch x p0' p1'+ | (p0', p1') <- shrink (p0, p1), p1' /= ZDD.empty+ ]++-- ------------------------------------------------------------------------+-- Union+-- ------------------------------------------------------------------------++prop_union_unitL :: Property+prop_union_unitL =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ ZDD.empty `ZDD.union` a === a++prop_union_unitR :: Property+prop_union_unitR =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ a `ZDD.union` ZDD.empty === a++prop_union_comm :: Property+prop_union_comm =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b) ->+ a `ZDD.union` b === b `ZDD.union` a++prop_union_assoc :: Property+prop_union_assoc =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b, c) ->+ a `ZDD.union` (b `ZDD.union` c) === (a `ZDD.union` b) `ZDD.union` c++prop_union_idempotent :: Property+prop_union_idempotent =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ a `ZDD.union` a === a++-- ------------------------------------------------------------------------+-- Intersection+-- ------------------------------------------------------------------------++prop_intersection_comm :: Property+prop_intersection_comm =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b) ->+ a `ZDD.intersection` b === b `ZDD.intersection` a++prop_intersection_assoc :: Property+prop_intersection_assoc =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b, c) ->+ a `ZDD.intersection` (b `ZDD.intersection` c) === (a `ZDD.intersection` b) `ZDD.intersection` c++prop_intersection_idempotent :: Property+prop_intersection_idempotent =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ a `ZDD.intersection` a === a++prop_intersection_emptyL :: Property+prop_intersection_emptyL =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ ZDD.empty `ZDD.intersection` a === ZDD.empty++prop_intersection_emptyR :: Property+prop_intersection_emptyR =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ a `ZDD.intersection` ZDD.empty === ZDD.empty++prop_intersection_distL :: Property+prop_intersection_distL =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b, c) ->+ a `ZDD.intersection` (b `ZDD.union` c) === (a `ZDD.intersection` b) `ZDD.union` (a `ZDD.intersection` c)++prop_intersection_distR :: Property+prop_intersection_distR =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b, c) ->+ (a `ZDD.union` b) `ZDD.intersection` c === (a `ZDD.intersection` c) `ZDD.union` (b `ZDD.intersection` c)++-- ------------------------------------------------------------------------+-- Difference+-- ------------------------------------------------------------------------++prop_difference_cancel :: Property+prop_difference_cancel =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ a ZDD.\\ a === ZDD.empty++prop_difference_unit :: Property+prop_difference_unit =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ a ZDD.\\ ZDD.empty === a++prop_union_difference :: Property+prop_union_difference =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b, c) ->+ (a `ZDD.union` b) ZDD.\\ c === (a ZDD.\\ c) `ZDD.union` (b ZDD.\\ c)++prop_difference_union :: Property+prop_difference_union =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b, c) ->+ a ZDD.\\ (b `ZDD.union` c) === (a ZDD.\\ b) ZDD.\\ c++-- ------------------------------------------------------------------------+-- Non-superset+-- ------------------------------------------------------------------------++prop_nonSuperset :: Property+prop_nonSuperset =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b) ->+ let a' = ZDD.toSetOfIntSets a+ b' = ZDD.toSetOfIntSets b+ p xs = and [not (IntSet.isSubsetOf ys xs) | ys <- Set.toList b']+ in ZDD.toSetOfIntSets (a `ZDD.nonSuperset` b) === Set.filter p a'++prop_nonSuperset_cancel :: Property+prop_nonSuperset_cancel =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ a `ZDD.nonSuperset` a === ZDD.empty++prop_nonSuperset_unit :: Property+prop_nonSuperset_unit =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ a `ZDD.nonSuperset` ZDD.empty === a++prop_union_nonSuperset :: Property+prop_union_nonSuperset =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b, c) ->+ (a `ZDD.union` b) `ZDD.nonSuperset` c === (a `ZDD.nonSuperset` c) `ZDD.union` (b `ZDD.nonSuperset` c)++prop_nonSuperset_union :: Property+prop_nonSuperset_union =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b, c) ->+ a `ZDD.nonSuperset` (b `ZDD.union` c) === (a `ZDD.nonSuperset` b) `ZDD.nonSuperset` c++prop_nonSuperset_difference :: Property+prop_nonSuperset_difference =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b) ->+ let c = a `ZDD.nonSuperset` b+ d = a ZDD.\\ b+ in counterexample (show (c, d)) $ c `ZDD.isSubsetOf` d++-- ------------------------------------------------------------------------+-- Minimal hitting sets+-- ------------------------------------------------------------------------++isHittingSetOf :: IntSet -> Set IntSet -> Bool+isHittingSetOf s g = all (\e -> not (IntSet.null (s `IntSet.intersection` e))) g++prop_minimalHittingSetsKnuth_isHittingSet :: Property+prop_minimalHittingSetsKnuth_isHittingSet =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ let b = ZDD.minimalHittingSetsKnuth a+ a' = ZDD.toSetOfIntSets a+ b' = ZDD.toSetOfIntSets b+ in all (`isHittingSetOf` a') b'++prop_minimalHittingSetsImai_isHittingSet :: Property+prop_minimalHittingSetsImai_isHittingSet =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ let b = ZDD.minimalHittingSetsImai a+ a' = ZDD.toSetOfIntSets a+ b' = ZDD.toSetOfIntSets b+ in all (`isHittingSetOf` a') b'++prop_minimalHittingSetsToda_isHittingSet :: Property+prop_minimalHittingSetsToda_isHittingSet =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ let b = ZDD.minimalHittingSetsToda a+ a' = ZDD.toSetOfIntSets a+ b' = ZDD.toSetOfIntSets b+ in all (`isHittingSetOf` a') b'++prop_minimalHittingSetsKnuth_duality :: Property+prop_minimalHittingSetsKnuth_duality =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ let b = ZDD.minimalHittingSetsKnuth a+ in ZDD.minimalHittingSetsKnuth (ZDD.minimalHittingSetsKnuth b) === b++prop_minimalHittingSetsImai_duality :: Property+prop_minimalHittingSetsImai_duality =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ let b = ZDD.minimalHittingSetsImai a+ in ZDD.minimalHittingSetsImai (ZDD.minimalHittingSetsImai b) === b++prop_minimalHittingSetsToda_duality :: Property+prop_minimalHittingSetsToda_duality =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ let b = ZDD.minimalHittingSetsToda a+ in ZDD.minimalHittingSetsToda (ZDD.minimalHittingSetsToda b) === b++prop_minimalHittingSets_Imai_equal_Knuth :: Property+prop_minimalHittingSets_Imai_equal_Knuth =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ ZDD.minimalHittingSetsImai a === ZDD.minimalHittingSetsKnuth a++prop_minimalHittingSets_Toda_equal_Knuth :: Property+prop_minimalHittingSets_Toda_equal_Knuth =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ ZDD.minimalHittingSetsToda a === ZDD.minimalHittingSetsKnuth a++-- ------------------------------------------------------------------------+-- Misc+-- ------------------------------------------------------------------------++prop_empty :: Property+prop_empty =+ forAllItemOrder $ \(_ :: Proxy o) ->+ ZDD.toSetOfIntSets (ZDD.empty :: ZDD o) === Set.empty++prop_base :: Property+prop_base =+ forAllItemOrder $ \(_ :: Proxy o) ->+ ZDD.toSetOfIntSets (ZDD.base :: ZDD o) === Set.singleton IntSet.empty++prop_singleton :: Property+prop_singleton =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll (liftM IntSet.fromList arbitrary) $ \xs ->+ let a :: ZDD o+ a = ZDD.singleton xs+ in counterexample (show a) $ ZDD.toSetOfIntSets a === Set.singleton xs++prop_subsets_member :: Property+prop_subsets_member =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \xs ->+ let a :: ZDD o+ a = ZDD.subsets xs+ in counterexample (show a) $ forAll (liftM IntSet.fromList (sublistOf (IntSet.toList xs))) $ \ys ->+ ys `ZDD.member` a++prop_subsets_member_empty :: Property+prop_subsets_member_empty =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \xs ->+ let a :: ZDD o+ a = ZDD.subsets xs+ in counterexample (show a) $ IntSet.empty `ZDD.member` a++prop_subsets_member_itself :: Property+prop_subsets_member_itself =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \xs ->+ let a :: ZDD o+ a = ZDD.subsets xs+ in counterexample (show a) $ xs `ZDD.member` a++prop_subsets_size :: Property+prop_subsets_size =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \xs ->+ let a :: ZDD o+ a = ZDD.subsets xs+ in counterexample (show a) $ ZDD.size a === (2 :: Integer) ^ (IntSet.size xs)++prop_toList_fromList :: Property+prop_toList_fromList =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \xss ->+ let a :: ZDD o+ a = Exts.fromList xss+ f = Set.fromList+ in counterexample (show a) $ f (Exts.toList a) === f xss++prop_fromList_toList :: Property+prop_fromList_toList =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ let xss = Exts.toList a+ in counterexample (show xss) $ Exts.fromList xss === a++prop_toSetOfIntSets_fromSetOfIntSets :: Property+prop_toSetOfIntSets_fromSetOfIntSets =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll (liftM (Set.fromList . map IntSet.fromList) arbitrary) $ \xss ->+ let a :: ZDD o+ a = ZDD.fromSetOfIntSets xss+ in counterexample (show a) $ ZDD.toSetOfIntSets a === xss++prop_fromSetOfIntSets_toSetOfIntSets :: Property+prop_fromSetOfIntSets_toSetOfIntSets =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ let xss = ZDD.toSetOfIntSets a+ in counterexample (show xss) $ ZDD.fromSetOfIntSets xss === a++prop_insert :: Property+prop_insert =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll (liftM IntSet.fromList arbitrary) $ \xs ->+ ZDD.toSetOfIntSets (ZDD.insert xs a) === Set.insert xs (ZDD.toSetOfIntSets a)++prop_insert_idempotent :: Property+prop_insert_idempotent =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll (liftM IntSet.fromList arbitrary) $ \xs ->+ let b = ZDD.insert xs a+ in counterexample (show b) $ ZDD.insert xs b === b++prop_delete :: Property+prop_delete =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll (liftM IntSet.fromList $ sublistOf (IntSet.toList (ZDD.flatten a))) $ \xs ->+ ZDD.toSetOfIntSets (ZDD.delete xs a) === Set.delete xs (ZDD.toSetOfIntSets a)++prop_delete_idempotent :: Property+prop_delete_idempotent =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll (liftM IntSet.fromList $ sublistOf (IntSet.toList (ZDD.flatten a))) $ \xs ->+ let b = ZDD.delete xs a+ in counterexample (show b) $ ZDD.delete xs b === b++prop_mapInsert :: Property+prop_mapInsert =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll arbitrary $ \x ->+ ZDD.toSetOfIntSets (ZDD.mapInsert x a) === Set.map (IntSet.insert x) (ZDD.toSetOfIntSets a)++prop_mapInsert_idempotent :: Property+prop_mapInsert_idempotent =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll arbitrary $ \x ->+ let b = ZDD.mapInsert x a+ in counterexample (show b) $ ZDD.mapInsert x b === b++prop_mapDelete :: Property+prop_mapDelete =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll arbitrary $ \x ->+ ZDD.toSetOfIntSets (ZDD.mapDelete x a) === Set.map (IntSet.delete x) (ZDD.toSetOfIntSets a)++prop_mapDelete_idempotent :: Property+prop_mapDelete_idempotent =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll arbitrary $ \x ->+ let b = ZDD.mapDelete x a+ in counterexample (show b) $ ZDD.mapDelete x b === b++prop_change :: Property+prop_change =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll arbitrary $ \x ->+ let f xs+ | IntSet.member x xs = IntSet.delete x xs+ | otherwise = IntSet.insert x xs+ in ZDD.toSetOfIntSets (ZDD.change x a) === Set.map f (ZDD.toSetOfIntSets a)++prop_change_involution :: Property+prop_change_involution =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll arbitrary $ \x ->+ ZDD.change x (ZDD.change x a) === a++prop_subset1 :: Property+prop_subset1 =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll arbitrary $ \x ->+ ZDD.toSetOfIntSets (ZDD.subset1 x a) === Set.map (IntSet.delete x) (Set.filter (IntSet.member x) (ZDD.toSetOfIntSets a))++prop_subset0 :: Property+prop_subset0 =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll arbitrary $ \x ->+ ZDD.toSetOfIntSets (ZDD.subset0 x a) === Set.filter (IntSet.notMember x) (ZDD.toSetOfIntSets a)++prop_member_1 :: Property+prop_member_1 =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ conjoin [counterexample (show xs) (ZDD.member xs a) | xs <- ZDD.toListOfIntSets a]++prop_member_2 :: Property+prop_member_2 =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ forAll (liftM IntSet.fromList $ sublistOf (IntSet.toList (ZDD.flatten a))) $ \s2 ->+ (s2 `ZDD.member` a) === (s2 `Set.member` ZDD.toSetOfIntSets a)++prop_size :: Property+prop_size =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ ZDD.size a === Set.size (ZDD.toSetOfIntSets a)++prop_null_size :: Property+prop_null_size =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ ZDD.null a === (ZDD.size a == (0 :: Int))++prop_isSubsetOf_refl :: Property+prop_isSubsetOf_refl =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ a `ZDD.isSubsetOf` a++prop_isSubsetOf_empty :: Property+prop_isSubsetOf_empty =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ ZDD.empty `ZDD.isSubsetOf` a++prop_isSubsetOf_and_isProperSubsetOf :: Property+prop_isSubsetOf_and_isProperSubsetOf =+ forAllItemOrder $ \(_ :: 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 =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ not (ZDD.isProperSubsetOf a a)++prop_disjoint :: Property+prop_disjoint =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o, b) ->+ ZDD.disjoint a b === ZDD.null (a `ZDD.intersection` b)++prop_flatten :: Property+prop_flatten =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ ZDD.flatten a === IntSet.unions (ZDD.toListOfIntSets a)++prop_uniformM :: Property+prop_uniformM =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll (arbitrary `suchThat` ((>= (2::Integer)) . ZDD.size)) $ \(a :: ZDD o) ->+ QM.monadicIO $ do+ gen <- QM.run Rand.create+ let m :: Integer+ m = ZDD.size a+ n = 1000+ samples <- QM.run $ replicateM n $ ZDD.uniformM a gen+ let hist_actual = Map.fromListWith (+) [(s, 1) | s <- samples]+ hist_expected = [(s, fromIntegral n / fromIntegral m) | s <- ZDD.toListOfIntSets a]+ chi_sq = sum [(Map.findWithDefault 0 s hist_actual - cnt) ** 2 / cnt | (s, cnt) <- hist_expected]+ threshold = complQuantile (chiSquared (fromIntegral m - 1)) 0.001+ QM.monitor $ counterexample $ show hist_actual ++ " /= " ++ show (Map.fromList hist_expected)+ QM.assert $ and [xs `ZDD.member` a | xs <- Map.keys hist_actual]+ QM.monitor $ counterexample $ "χ² = " ++ show chi_sq ++ " >= " ++ show threshold+ QM.assert $ chi_sq < threshold++prop_findMinSum :: Property+prop_findMinSum =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll (arbitrary `suchThat` (not . ZDD.null)) $ \(a :: ZDD o) ->+ forAll arbitrary $ \(weight' :: Fun Int Integer) ->+ let weight = apply weight'+ setWeight s = sum [weight x | x <- IntSet.toList s]+ (obj0, s0) = ZDD.findMinSum weight a+ in counterexample (show [(x, weight x) | x <- IntSet.toList (ZDD.flatten a)]) $+ counterexample (show (obj0, s0)) $+ setWeight s0 === obj0+ .&&.+ conjoin [counterexample (show (s, setWeight s)) $ obj0 <= setWeight s | s <- ZDD.toListOfIntSets a]++prop_findMaxSum :: Property+prop_findMaxSum =+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll (arbitrary `suchThat` (not . ZDD.null)) $ \(a :: ZDD o) ->+ forAll arbitrary $ \(weight' :: Fun Int Integer) ->+ let weight = apply weight'+ setWeight s = sum [weight x | x <- IntSet.toList s]+ (obj0, s0) = ZDD.findMaxSum weight a+ in counterexample (show [(x, weight x) | x <- IntSet.toList (ZDD.flatten a)]) $+ counterexample (show (obj0, s0)) $+ setWeight s0 === obj0+ .&&.+ conjoin [counterexample (show (s, setWeight s)) $ obj0 >= setWeight s | s <- ZDD.toListOfIntSets a]++-- ------------------------------------------------------------------------++prop_toGraph_fromGraph :: Property+prop_toGraph_fromGraph = do+ forAllItemOrder $ \(_ :: Proxy o) ->+ forAll arbitrary $ \(a :: ZDD o) ->+ ZDD.fromGraph (ZDD.toGraph a) === a++-- ------------------------------------------------------------------------+-- Test cases from JDD library+-- https://bitbucket.org/vahidi/jdd/src/21e103689c697fa40022294a829cab04add8ff79/src/jdd/zdd/ZDD.java++case_jdd_test_1 :: Assertion+case_jdd_test_1 = do+ let x1 = 1+ x2 = 2++ a, b, c, d, e, f, g :: ZDD ZDD.DescOrder+ a = ZDD.empty -- {}+ b = ZDD.base -- {{}}+ c = ZDD.change x1 b -- {{x1}}+ d = ZDD.change x2 b -- {{x2}}+ e = ZDD.union c d -- {{x1}, {x2}}+ f = ZDD.union b e -- {{}, {x1}, {x2}}+ g = ZDD.difference f c -- {{}, {x2}}++ -- directly from minatos paper, figure 9+ -- [until we find a better way to test isomorphism...]+ a @?= ZDD.Empty+ b @?= ZDD.Base+ c @?= ZDD.Branch x1 ZDD.empty ZDD.base+ d @?= ZDD.Branch x2 ZDD.empty ZDD.base+ e @?= ZDD.Branch x2 c ZDD.base+ f @?= ZDD.Branch x2 (ZDD.Branch x1 ZDD.base ZDD.base) ZDD.base+ g @?= ZDD.Branch x2 ZDD.base ZDD.base++ -- intersect+ ZDD.intersection a b @?= a+ ZDD.intersection a ZDD.base @?= a+ ZDD.intersection b b @?= b+ ZDD.intersection c e @?= c+ ZDD.intersection e f @?= e+ ZDD.intersection e g @?= d++ -- union+ ZDD.union a a @?= a+ ZDD.union b b @?= b+ ZDD.union a b @?= b+ ZDD.union g e @?= f++ -- diff+ ZDD.difference a a @?= a+ ZDD.difference b b @?= a+ ZDD.difference d c @?= d+ ZDD.difference c d @?= c+ ZDD.difference e c @?= d+ ZDD.difference e d @?= c+ ZDD.difference g b @?= d++ ZDD.difference g d @?= b+ ZDD.difference f g @?= c+ ZDD.difference f e @?= b++ -- subset0+ ZDD.subset0 x1 b @?= b+ ZDD.subset0 x2 b @?= b+ ZDD.subset0 x2 d @?= a+ ZDD.subset0 x2 e @?= c++ -- subset1+ ZDD.subset1 x1 b @?= ZDD.empty+ ZDD.subset1 x2 b @?= ZDD.empty+ ZDD.subset1 x2 d @?= b+ ZDD.subset1 x2 g @?= b+ ZDD.subset1 x1 g @?= a+ ZDD.subset1 x2 e @?= b++case_jdd_test_2 :: Assertion+case_jdd_test_2 = do+ let [a, b, c, d] = [4, 3, 2, 1]++ -- this is the exact construction sequence of Fig.14 in "Zero-suppressed BDDs and their application" by Minato+ let fig14 :: ZDD ZDD.DescOrder+ fig14 = ZDD.union z00__ z0100+ where+ z0000 = ZDD.base+ z000_ = ZDD.union z0000 (ZDD.change d z0000)+ z00__ = ZDD.union z000_ (ZDD.change c z000_)+ z0100 = ZDD.change b z0000++ -- this is the exact construction sequence of Fig.13 in "Zero-suppressed BDDs and their application" by Minato+ let fig13 :: ZDD ZDD.DescOrder+ fig13 = ZDD.intersection z0___ tmp+ where+ z___0 = ZDD.subsets (IntSet.fromList [a, b, c])+ z__0_ = ZDD.subsets (IntSet.fromList [a, b, d])+ z_0__ = ZDD.subsets (IntSet.fromList [a, c, d])+ z0___ = ZDD.subsets (IntSet.fromList [b, c, d])+ z__00 = ZDD.intersection z___0 z__0_+ tmp = ZDD.union z_0__ z__00++ fig14 @?= fig13++case_jdd_test_3 :: Assertion+case_jdd_test_3 = do+ let tmp :: ZDD ZDD.DescOrder+ tmp = ZDD.fromListOfIntSets $ map IntSet.fromList [[2], [0,1], [1]] -- "100 011 010"+ tmp2 = ZDD.union (ZDD.singleton (IntSet.fromList [0, 1])) ZDD.base -- union("11", base)+ -- 1. INTERSECT+ ZDD.intersection tmp tmp2 @?= ZDD.singleton (IntSet.fromList [0, 1])+ -- 2. UNION+ ZDD.union tmp tmp2 @?= ZDD.union tmp ZDD.base+ -- 3. DIFF+ ZDD.difference tmp tmp2 @?= ZDD.fromListOfIntSets (map IntSet.fromList [[1], [2]])++-- ------------------------------------------------------------------------++zddTestGroup :: TestTree+zddTestGroup = $(testGroupGenerator)
+ test/Utils.hs view
@@ -0,0 +1,24 @@+{-# LANGUAGE RankNTypes #-}+module Utils+ ( forAllItemOrder+ ) where++import Data.Proxy+import Test.QuickCheck++import Data.DecisionDiagram.BDD.Internal.ItemOrder++data SomeItemOrder+ = AscOrder+ | DescOrder+ deriving (Show, Enum, Bounded)++instance Arbitrary SomeItemOrder where+ arbitrary = arbitraryBoundedEnum++forAllItemOrder :: Testable prop => (forall o. ItemOrder o => Proxy o -> prop) -> Property+forAllItemOrder k =+ forAll arbitrary $ \o ->+ case o of+ AscOrder -> withAscOrder k+ DescOrder -> withDescOrder k