diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,3 @@ +# Changelog for decision-diagrams + +## Unreleased changes diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,8 @@ +# decision-diagrams + +[![Build Status](https://github.com/msakai/haskell-decision-diagrams/actions/workflows/build.yaml/badge.svg)](https://github.com/msakai/haskell-decision-diagrams/actions/workflows/build.yaml) +[![Coverage Status](https://coveralls.io/repos/msakai/haskell-decision-diagrams/badge.svg)](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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/decision-diagrams.cabal b/decision-diagrams.cabal new file mode 100644 --- /dev/null +++ b/decision-diagrams.cabal @@ -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 +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 diff --git a/src/Data/DecisionDiagram/BDD.hs b/src/Data/DecisionDiagram/BDD.hs new file mode 100644 --- /dev/null +++ b/src/Data/DecisionDiagram/BDD.hs @@ -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). +-- +-- +---------------------------------------------------------------------- +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))))))) +-} + +-- ------------------------------------------------------------------------ diff --git a/src/Data/DecisionDiagram/BDD/Internal/ItemOrder.hs b/src/Data/DecisionDiagram/BDD/Internal/ItemOrder.hs new file mode 100644 --- /dev/null +++ b/src/Data/DecisionDiagram/BDD/Internal/ItemOrder.hs @@ -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 + +-- ------------------------------------------------------------------------ diff --git a/src/Data/DecisionDiagram/BDD/Internal/Node.hs b/src/Data/DecisionDiagram/BDD/Internal/Node.hs new file mode 100644 --- /dev/null +++ b/src/Data/DecisionDiagram/BDD/Internal/Node.hs @@ -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_ + +-- ------------------------------------------------------------------------ diff --git a/src/Data/DecisionDiagram/ZDD.hs b/src/Data/DecisionDiagram/ZDD.hs new file mode 100644 --- /dev/null +++ b/src/Data/DecisionDiagram/ZDD.hs @@ -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). +-- +-- +---------------------------------------------------------------------- +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: . +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: . +-- +-- * HTC-BDD: Hypergraph Transversal Computation with Binary Decision Diagrams +-- +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' + +-- ------------------------------------------------------------------------ diff --git a/test/TestBDD.hs b/test/TestBDD.hs new file mode 100644 --- /dev/null +++ b/test/TestBDD.hs @@ -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) diff --git a/test/TestSuite.hs b/test/TestSuite.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite.hs @@ -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 + ] diff --git a/test/TestZDD.hs b/test/TestZDD.hs new file mode 100644 --- /dev/null +++ b/test/TestZDD.hs @@ -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) diff --git a/test/Utils.hs b/test/Utils.hs new file mode 100644 --- /dev/null +++ b/test/Utils.hs @@ -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