HasCacBDD 0.1.0.3 → 0.1.0.4
raw patch · 5 files changed
+30/−25 lines, 5 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- HasCacBDD.cabal +2/−2
- README.md +0/−1
- hs/Data/HasCacBDD.hs +15/−10
- stack.yaml +1/−1
- tests/Main.hs +12/−11
HasCacBDD.cabal view
@@ -1,5 +1,5 @@ name: HasCacBDD-version: 0.1.0.3+version: 0.1.0.4 synopsis: Haskell bindings for CacBDD homepage: https://github.com/m4lvin/HasCacBDD license: GPL-2@@ -31,7 +31,7 @@ custom-setup setup-depends: base >= 4.8 && < 5,- Cabal,+ Cabal < 3.9, directory library
README.md view
@@ -3,7 +3,6 @@ [](https://github.com/m4lvin/HasCacBDD/releases) [](https://hackage.haskell.org/package/HasCacBDD)-[](https://travis-ci.org/m4lvin/HasCacBDD) Haskell bindings for CacBDD, a Binary Decision Diagram (BDD) package with dynamic cache management.
hs/Data/HasCacBDD.hs view
@@ -26,10 +26,11 @@ maximumvar, showInfo ) where -import Foreign.C+import Control.Arrow (Arrow(first))+import Foreign.C (CInt(..)) import Foreign.Ptr (Ptr) import Foreign (ForeignPtr, newForeignPtr, withForeignPtr, finalizerFree)-import System.IO.Unsafe+import System.IO.Unsafe (unsafePerformIO) import Data.List (nub,(\\),sort) import Data.Maybe (fromJust) import Test.QuickCheck (Arbitrary, Gen, arbitrary, shrink, choose, oneof, sized, listOf)@@ -278,22 +279,26 @@ allVarsOfSorted :: Bdd -> [Int] allVarsOfSorted = sort . allVarsOf --- | List all the sub-BDDs of a given BDD.+-- | List all node / sub-BDDs of a given BDD.+-- This includes the root node of b itself, but omits terminal nodes. subsOf :: Bdd -> [Bdd]-subsOf b- | b == bot = []- | b == top = []- | otherwise = nub $ b : (subsOf (thenOf b) ++ subsOf (elseOf b))+subsOf = subsOf' [] where+ subsOf' done b+ | b == bot = done+ | b == top = done+ | b `elem` done = done+ | otherwise = let intermedDone = subsOf' done (thenOf b)+ in b : subsOf' intermedDone (elseOf b) --- | Size of the BDD, should be the number of non-terminal nodes.+-- | Size of the BDD, the number of non-terminal nodes. sizeOf :: Bdd -> Int-sizeOf = length.subsOf+sizeOf = length . subsOf instance Show Bdd where show = show . unravel instance Read Bdd where- readsPrec k input = map (\(a,s) -> (ravel a, s)) (readsPrec k input)+ readsPrec k input = map (first ravel) (readsPrec k input) -- | A simple tree definition to show BDDs as text. data BddTree = Bot | Top | Var Int BddTree BddTree deriving (Eq,Read,Show)
stack.yaml view
@@ -1,3 +1,3 @@-resolver: lts-16.1+resolver: lts-18.21 packages: - '.'
tests/Main.hs view
@@ -13,10 +13,10 @@ describe "Examples" $ do describe "Creating BDDs" $ do it "top == Top" $ show top `shouldBe` "Top"- it "" $ show bot `shouldBe` "Bot"- it "" $ show (var 1) `shouldBe` "Var 1 Top Bot"- it "" $ show (var 1) `shouldBe` "Var 1 Top Bot"- it "" $ show (var 2) `shouldBe` "Var 2 Top Bot"+ it "show bot" $ show bot `shouldBe` "Bot"+ it "show (var 1)" $ show (var 1) `shouldBe` "Var 1 Top Bot"+ it "show (var 2)" $ show (var 1) `shouldBe` "Var 1 Top Bot"+ it "show (var 3)" $ show (var 2) `shouldBe` "Var 2 Top Bot" describe "Some tautologies" $ do it "bot == bot" $ bot `shouldBe` bot it "top == top" $ top `shouldBe` top@@ -37,8 +37,8 @@ it "var 1 /= var 2" $ var 1 `shouldNotBe` var 2 it "forall 1 (var 1) /= top" $ forall 1 (var 1) `shouldNotBe` top describe "Laws from de Morgan:" $ do- it "" $ dis (neg $ var 1) (neg $ var 2) == neg (con (var 1) (var 2))- it "" $ con (neg $ var 1) (neg $ var 2) == neg (dis (var 1) (var 2))+ it "dis to con" $ dis (neg $ var 1) (neg $ var 2) == neg (con (var 1) (var 2))+ it "con to dis" $ con (neg $ var 1) (neg $ var 2) == neg (dis (var 1) (var 2)) it "The example from CacBDDs main.cpp (~x[4] + ~x[6]) * (~x[3] + ~x[6]) * (~x[2] + ~x[5]) /= top" $ conSet [ dis (neg (var 4)) (neg (var 6)) , neg (var 3) `dis` neg (var 6), neg (var 2) `dis` neg (var 5) ] `shouldNotBe` top it "showInfo works" $@@ -46,7 +46,7 @@ describe "Basics" $ do it "top == top" $ top `shouldBe` top it "top /= bot" $ top `shouldNotBe` bot- it "bo /= top" $ bot `shouldNotBe` top+ it "bot /= top" $ bot `shouldNotBe` top it "bot == bot" $ bot `shouldBe` bot it "neg bot == top" $ neg bot `shouldBe` top it "neg bot /= bot" $ neg bot `shouldNotBe` bot@@ -95,20 +95,21 @@ prop "deMorganTwoSet" (\as -> neg (disSet as) == conSet (map neg as)) prop "conSetCommute" (\a as -> conSet (a:as) == con (conSet as) a) prop "disSetCommute" (\a as -> disSet (a:as) == dis (disSet as) a)- prop "xor-disSet" ( (\as -> xorSet as `imp` disSet as == top) . (take 23) )+ prop "xor-disSet" ( (\as -> xorSet as `imp` disSet as == top) . take 23 ) prop "xorSetNeg3" (\a b c -> xorSet [a,b,c] == xorSet [neg a, b, neg c]) prop "xorSetCommute3" (\a b c -> xorSet [a,b,c] == xor (xorSet [a,b]) c) prop "xorSetCommute4" (\a b c d -> xorSet [a,b,c,d] == xor (xorSet [b,c,a]) d) prop "gfpCon" (\b -> gfp (`con` b) == b)- prop "sizeNeg" (\b -> sizeOf b == sizeOf (neg b))+ prop "sizeOf neg" (\b -> sizeOf b == sizeOf (neg b)) prop "restrictLaw" (\a b -> b `imp` equ (restrictLaw a b) a == top) prop "evaluate" (\b -> all (\s -> evaluate b s == Just True) (allSatsWith (allVarsOf b) b)) prop "evaluateFun" (\b -> all (\s -> evaluateFun b (\n -> fromJust $ lookup n s)) (allSats b))- prop "evaluateFun F" (\b -> all (\s -> not (evaluateFun bot (\n -> fromJust $ lookup n s))) (allSats b))+ prop "evaluateFun F" (all (\s -> not (evaluateFun bot (\n -> fromJust $ lookup n s))) . allSats) prop "allSatsWith" (\b -> all (\s -> restrictSet b s == top) (allSatsWith (allVarsOf b) b)) prop "anySatWith" (\b -> let vs = allVarsOf b in if b==bot then isNothing (anySatWith vs b) else restrictSet b (fromJust $ anySatWith vs b) == top) prop "satCountWith" (\b -> let vs = allVarsOf b in length (allSatsWith vs b) == satCountWith vs b) prop "subsOf" (\b -> all (`elem` subsOf b) (subsOf $ thenOf b))+ prop "subsOf" (\b -> all (`elem` subsOf b) (subsOf $ elseOf b)) prop "relabel" (\b c -> let vs = reverse $ nub (allVarsOf b ++ allVarsOf c) mapping = zip vs (map (+100) vs)@@ -120,7 +121,7 @@ prop "show" (\a b -> (show a == show b) == (a == (b::Bdd))) prop "read" (\b -> read (show b) == (b :: Bdd)) prop "showList" (\a b -> (showList [unravel a] "" == showList [unravel b] "") == (a == (b::Bdd)))- prop "readList" (\a b -> (readList (show [a,b]) == [([unravel a, unravel b] :: [BddTree], "")]))+ prop "readList" (\a b -> readList (show [a,b]) == [([unravel a, unravel b] :: [BddTree], "")]) describe "QuickCheck Expected Failures" $ do prop "wrong deMorganOne" $ expectFailure (\a b -> neg (a `con` b) === (neg a `con` neg b))