diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,9 @@ # HasCacBDD Changelog +## v0.4.0.0 (2026-06-20) + +- rewrite "Show" and "Read" instances using "top", "bot", "var", "ifthenelse" and parsec for "Read". This should make them lawful. + ## v0.3.0.1 (2025-10-22) - let `svgGraph` try to find the `dot` executable in multiple common locations. This should make it work on non-Linux systems. (Thanks to @MitchBoontjes for the original patch.) diff --git a/HasCacBDD.cabal b/HasCacBDD.cabal --- a/HasCacBDD.cabal +++ b/HasCacBDD.cabal @@ -1,5 +1,5 @@ name: HasCacBDD -version: 0.3.0.1 +version: 0.4.0.0 synopsis: Haskell bindings for CacBDD homepage: https://github.com/m4lvin/HasCacBDD license: GPL-2 @@ -30,7 +30,7 @@ source-repository head type: git - location: git://github.com/m4lvin/HasCacBDD.git + location: https://github.com/m4lvin/HasCacBDD.git custom-setup setup-depends: base >= 4.8 && < 5, @@ -41,6 +41,7 @@ exposed-modules: Data.HasCacBDD, Data.HasCacBDD.Visuals build-depends: base >=4.8 && < 5, + parsec >= 3.1 && < 3.2, process >= 1.1 && < 1.7, QuickCheck >= 2.4 && < 2.15, directory < 1.4 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -33,12 +33,14 @@ 3. Now you can play with Boolean functions :-) - λ> import Data.HasCacBDD - λ> var 5 - Var 5 Top Bot - λ> neg (var 5) - Var 5 Bot Top - λ> dis (neg (var 3)) (var 3) - Top + ghci> import Data.HasCacBDD + ghci> var 5 + var 5 + ghci> neg (var 5) + neg (var 5) + ghci> dis (neg (var 3)) (var 3) + top + ghci> dis (neg (var 1)) (var 3) + ifthenelse (var 1) (var 3) top For further documentation, see diff --git a/hs/Data/HasCacBDD.hs b/hs/Data/HasCacBDD.hs --- a/hs/Data/HasCacBDD.hs +++ b/hs/Data/HasCacBDD.hs @@ -28,7 +28,6 @@ maximumvar, showInfo ) where -import Control.Arrow (Arrow(first)) import Foreign.C (CInt(..)) import Foreign.Ptr (Ptr) import Foreign (ForeignPtr, newForeignPtr, withForeignPtr, finalizerFree) @@ -37,6 +36,7 @@ import Data.List ((\\), minimumBy, nub, permutations, sort) import Data.Maybe (fromJust, listToMaybe) import Test.QuickCheck (Arbitrary, Gen, arbitrary, shrink, choose, oneof, sized, listOf) +import Text.Parsec -- | The CacBDD datatype has no structure because -- from our perspective BDDs are just pointers. @@ -308,12 +308,29 @@ sizeOf = length . subsOf instance Show Bdd where - show = show . unravel + showsPrec d b = f (d > 10) (unravel b) where + f :: Bool -> BddTree -> ShowS + f _ Bot = ("bot" ++) + f _ Top = ("top" ++) + f p (Var n Top Bot) = showParen p (("var " ++ show n) ++) + f p (Var n Bot Top) = showParen p (("neg (var " ++ show n ++ ")") ++) + f p (Var n a c) = showParen p + (("ifthenelse (var " ++ show n ++ ") " ++ f True a "" ++ " " ++ f True c "") ++) instance Read Bdd where - readsPrec k input = map (first ravel) (readsPrec k input) + readsPrec _ input = either (const []) return (parse pBdd "" input) --- | A simple tree definition to show BDDs as text. +-- | Parser for 'Bdd' values, used by the 'Read' instance. +pBdd :: Parsec String () (Bdd,String) +pBdd = (,) <$> pExp <*> getInput where -- No "<* eof" here, but getInput for readList. + pExp = spaces >> (pAtom <|> pIfThenElse <|> pNeg) + pAtom = (pConst <|> pVar <|> (char '(' *> pExp <* char ')')) <* spaces + pConst = (string "top" >> return top) <|> (string "bot" >> return bot) + pVar = string "var " >> (var . read <$> many1 digit) + pNeg = string "neg " >> neg <$> pAtom + pIfThenElse = string "ifthenelse " >> spaces >> ifthenelse <$> pAtom <*> pAtom <*> pAtom + +-- | A tree definition that is also used to 'show' values ot the 'Bdd' type. data BddTree = Bot | Top | Var Int BddTree BddTree deriving (Eq,Read,Show) -- | Convert a BDD to a tree. diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,6 +1,6 @@ {-# OPTIONS_GHC -Wno-x-partial #-} -module Main where +module Main (main) where import Data.List ((\\),nub) import Data.Maybe (fromJust,isNothing) @@ -15,12 +15,12 @@ main :: IO () main = hspec $ do describe "Examples" $ do - describe "Creating BDDs" $ do - it "top == Top" $ show top `shouldBe` "Top" - 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 "Creating and showing BDDs" $ do + it "top == Top" $ show top `shouldBe` "top" + it "show bot" $ show bot `shouldBe` "bot" + it "show (var 1)" $ show (var 1) `shouldBe` "var 1" + it "show (var 2)" $ show (var 1) `shouldBe` "var 1" + it "show (var 3)" $ show (var 2) `shouldBe` "var 2" describe "Some tautologies" $ do it "bot == bot" $ bot `shouldBe` bot it "top == top" $ top `shouldBe` top @@ -67,12 +67,11 @@ it "imp (conSet [var 1,var 0]) (var 1) == top" $ imp (conSet [var 1,var 0]) (var 1) `shouldBe` top it "imp (conSet [var 0,var 1]) (var 0) == top" $ imp (conSet [var 0,var 1]) (var 0) `shouldBe` top it "imp (con (var 0) (var 1)) (var 0) == top" $ imp (con (var 0) (var 1)) (var 0) `shouldBe` top - it "show top == \"Top\"" $ show top `shouldBe` "Top" - it "show bot == \"Bot\"" $ show bot `shouldBe` "Bot" + it "show top == \"top\"" $ show top `shouldBe` "top" + it "show bot == \"bot\"" $ show bot `shouldBe` "bot" describe "QuickCheck Properties" $ do prop "selfEqual" (\b -> (b::Bdd) == b) prop "showReadEqual" (\b -> read (show b) == (b::Bdd)) - prop "showReadTreeEq" (\b -> (ravel . read . show . unravel $ b) == b) prop "idSymmetry" (\a b -> ((a::Bdd) == (b::Bdd)) == (b == a)) prop "singleNegation" (\b -> neg b /= b) prop "doubleNegation" (\b -> neg (neg b) == b) @@ -90,7 +89,6 @@ prop "allSats" (\b -> all (\s -> restrictSet b s == top) (allSats b)) prop "anySat" (\b -> if b==bot then isNothing (anySat b) else restrictSet b (fromJust $ anySat b) == top) prop "ifthenelse" (\a b c -> ifthenelse a b c == neg (dis (con a (neg b)) (con (neg a) (neg c)))) - prop "ravel-unravel" (\b -> b == ravel (unravel b)) prop "firstVarOf" (\b -> if b `elem` [bot,top] then isNothing (firstVarOf b) else Just (head (allVarsOfSorted b)) == firstVarOf b) prop "maxVarOf" (\b -> if b `elem` [bot,top] then isNothing (maxVarOf b) else Just (last (allVarsOfSorted b)) == maxVarOf b) prop "thenOf" (\b -> if b `elem` [bot,top] then thenOf b == b else thenOf b == restrict b (fromJust $ firstVarOf b, True )) @@ -120,16 +118,20 @@ gnippam = map swap mapping in relabel gnippam (relabel mapping b) == b) - prop "relabelFun" (\a -> relabelFun (\x -> x-7) (relabelFun (+7) a) == a) - prop "substit" (\b c -> substit 5 b c == ifthenelse b (restrict c (5,True)) (restrict c (5,False))) - prop "substit2" (\b c -> substit (head ([0..] \\ allVarsOf c)) b c == c) - prop "substitSimul" (\b -> substitSimul [] b == b) - prop "substitSimul2" (\b n -> substitSimul [(n,var n)] b == b) + prop "relabelFun" (\a -> relabelFun (\x -> x-7) (relabelFun (+7) a) === a) + prop "substit" (\b c -> substit 5 b c === ifthenelse b (restrict c (5,True)) (restrict c (5,False))) + prop "substit2" (\b c -> substit (head ([0..] \\ allVarsOf c)) b c === c) + prop "substitSimul" (\b -> substitSimul [] b === b) + prop "substitSimul2" (\b n -> substitSimul [(n,var n)] b === b) prop "optimalOrder" (\b -> sizeOf b < 15 ==> sizeOf (relabel (optimalOrder b) b) <= sizeOf b) - 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], "")]) + describe "Unraveling to BddTree" $ do + prop "ravel-unravel" (\b -> b == ravel (unravel b)) + prop "ravel-unravelN" (\b -> b /= ravel (unravel (neg b))) + prop "showReadTreeEq" (\b -> (ravel . read . show . unravel $ b) == b) + prop "treeShowReadEq" (\b -> (read . show . unravel $ b) == unravel b) + prop "treeEqIffEq" (\a b -> (unravel a == unravel b) === (a == b)) + prop "treeNEqIffEq" (\a b -> (unravel a /= unravel b) === (a /= b)) + prop "listShowRead" (\a b c -> (read . show . map unravel $ [a,b,c]) == map unravel [a, b, c]) describe "QuickCheck Expected Failures" $ do prop "evaluate may return Nothing" $ expectFailure (\b ass -> evaluate b ass =/= Nothing) @@ -152,3 +154,24 @@ (svgGraph top >>= \ s -> return (length s < 1000)) `shouldReturn` True it "svgGraph (var 1) is longer" $ (svgGraph (var 1) >>= \ s -> return (length s > 1000)) `shouldReturn` True + describe "instances Show Bdd and Read Bdd" $ do + describe "show" $ do + it "var 1 `con` var 2" $ show (var 1 `con` var 2) `shouldBe` "ifthenelse (var 1) (var 2) bot" + prop "show ==" (\a b -> (show a == show b) === (a == (b::Bdd))) + prop "read ==" (\b -> read (show b) === (b :: Bdd)) + describe "Pair for precendence test" $ do + it "show (P (var 3) top)" $ show (P (var 3) top) `shouldBe` "P (var 3) top" + it "show (P (var 3) (var 1 `con` var 2))" $ show (P (var 3) (var 1 `con` var 2)) `shouldBe` "P (var 3) (ifthenelse (var 1) (var 2) bot)" + describe "showList" $ do + prop "showList [a]" (\a b -> (showList [a] "" == showList [b] "") === (a == (b::Bdd))) + prop "readList [a,b]" (\a b -> readList (show [a,b]) === [([a, b] :: [Bdd], "")]) + prop "readList [...]" (\l -> readList (show l) === [(l :: [Bdd], "")]) + describe "instance Read Bdd" $ do + describe "single BDD value" $ do + it "read \"var 1\"" $ read "var 1" `shouldBe` var 1 + it "read \"ifthenelse (var 1) (var 2) (var 2)\"" $ read "ifthenelse (var 1) (var 2) (var 2)" `shouldBe` ifthenelse (var 1) (var 2) (var 2) + describe "list of BDDs" $ do + it "read \"[var 1, var 3]\"" $ read "[var 1, var 3]" `shouldBe` [var 1, var 3] + it "read \"[ top , ifthenelse ( var 3 ) bot bot]\"" $ read "[ top , ifthenelse ( var 3 ) bot bot]" `shouldBe` [top, bot] + +data Pair = P Bdd Bdd deriving (Show)