HasCacBDD 0.2.0.0 → 0.4.0.0
raw patch · 9 files changed
Files
- CHANGELOG.md +13/−2
- HasCacBDD.cabal +7/−5
- README.md +13/−9
- c/BDDNodeC.cpp +21/−21
- c/BDDNodeC.h +23/−21
- hs/Data/HasCacBDD.hs +62/−28
- hs/Data/HasCacBDD/Visuals.hs +34/−8
- stack.yaml +1/−1
- tests/Main.hs +65/−19
CHANGELOG.md view
@@ -1,8 +1,19 @@ # HasCacBDD Changelog -## upcoming+## 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.)+- add tests for `Data.HasCacBDD.Visuals` module.++## v0.3.0.0 (2025-01-01)++- add `optimalOrder`+- fix segfault on Apple M1 and ARM aarch64+- minor improvements of documentation and tests ## v0.2.0.0 (2023-11-23)
HasCacBDD.cabal view
@@ -1,5 +1,5 @@ name: HasCacBDD-version: 0.2.0.0+version: 0.4.0.0 synopsis: Haskell bindings for CacBDD homepage: https://github.com/m4lvin/HasCacBDD license: GPL-2@@ -30,19 +30,21 @@ 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,- Cabal < 3.9,- directory+ Cabal < 3.13,+ directory <1.4 library 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+ QuickCheck >= 2.4 && < 2.15,+ directory < 1.4 default-language: Haskell2010 hs-source-dirs: hs extra-libraries: stdc++, CacBDD
README.md view
@@ -3,8 +3,8 @@ [](https://github.com/m4lvin/HasCacBDD/releases) [](https://hackage.haskell.org/package/HasCacBDD)-[](https://gitlab.com/m4lvin/HasCacBDD/-/pipelines)-[](https://gitlab.com/m4lvin/HasCacBDD/-/jobs/artifacts/master/file/hpc/combined/all/hpc_index.html?job=test)+[](https://gitlab.com/m4lvin/HasCacBDD/-/pipelines)+[](https://gitlab.com/m4lvin/HasCacBDD/-/jobs/artifacts/main/file/hpc/combined/all/hpc_index.html?job=test) Haskell bindings for CacBDD, a Binary Decision Diagram (BDD) package with dynamic cache management. @@ -33,10 +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 <https://hackage.haskell.org/package/HasCacBDD/docs/Data-HasCacBDD.html>
c/BDDNodeC.cpp view
@@ -7,21 +7,21 @@ int BDD_Variable(BDD* this_ptr) { return this_ptr->Variable(); } -BDD BDD_Then(const BDD* this_ptr) { return this_ptr->Then(); }+void BDD_Then(BDD* ret_ptr, const BDD* this_ptr) { *ret_ptr = this_ptr->Then(); } -BDD BDD_Else(const BDD* this_ptr) { return this_ptr->Else(); }+void BDD_Else(BDD* ret_ptr, const BDD* this_ptr) { *ret_ptr = this_ptr->Else(); } -BDD BDD_Exist(BDD* this_ptr, const BDD* cube) { return this_ptr->Exist(*cube); }+void BDD_Exist(BDD* ret_ptr, BDD* this_ptr, const BDD* cube) { *ret_ptr = this_ptr->Exist(*cube); } -BDD BDD_Universal(BDD* this_ptr, const BDD* cube) { return this_ptr->Universal(*cube); }+void BDD_Universal(BDD* ret_ptr, BDD* this_ptr, const BDD* cube) { *ret_ptr = this_ptr->Universal(*cube); } -BDD BDD_Restrict(const BDD* this_ptr, const BDD* other) { return this_ptr->Restrict(*other); }+void BDD_Restrict(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = this_ptr->Restrict(*other); } -BDD BDD_Compose(const BDD* this_ptr, int v, const BDD* other) { return this_ptr->Compose(v, *other); }+void BDD_Compose(BDD* ret_ptr, const BDD* this_ptr, int v, const BDD* other) { *ret_ptr = this_ptr->Compose(v, *other); } -BDD BDD_Permute(const BDD* this_ptr, const vector<int>* permu) { return this_ptr->Permute(*permu); }+void BDD_Permute(BDD* ret_ptr, const BDD* this_ptr, const vector<int>* permu) { *ret_ptr = this_ptr->Permute(*permu); } -BDD BDD_AndExist(BDD* this_ptr, const BDD* other, const BDD* cube) { return this_ptr->AndExist(*other, *cube); }+void BDD_AndExist(BDD* ret_ptr, BDD* this_ptr, const BDD* other, const BDD* cube) { *ret_ptr = this_ptr->AndExist(*other, *cube); } bool BDD_IsComp(BDD* this_ptr) { bool b = this_ptr->IsComp(); return b; } @@ -29,32 +29,32 @@ XBDDManager* XBDDManager_new(int varCount) { return new XBDDManager(varCount); } -BDD XBDDManager_BddOne(XBDDManager* this_ptr) { return (BDD) this_ptr->BddOne(); }+void XBDDManager_BddOne(BDD* ret_ptr, XBDDManager* this_ptr) { *ret_ptr = this_ptr->BddOne(); } -BDD XBDDManager_BddZero(XBDDManager* this_ptr) { return (BDD) this_ptr->BddZero(); }+void XBDDManager_BddZero(BDD* ret_ptr, XBDDManager* this_ptr) { *ret_ptr = this_ptr->BddZero(); } -BDD XBDDManager_BddVar(XBDDManager* this_ptr, int varIndex) { BDD bar = this_ptr->BddVar(varIndex); return bar; }+void XBDDManager_BddVar(BDD* ret_ptr, XBDDManager* this_ptr, int varIndex) { *ret_ptr = this_ptr->BddVar(varIndex); } -BDD XBDDManager_Ite(XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h) { return (BDD) this_ptr->Ite(*f, *g, *h); }+void XBDDManager_Ite(BDD* ret_ptr, XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h) { *ret_ptr = this_ptr->Ite(*f, *g, *h); } const XManager* XBDDManager_manager(const XBDDManager* this_ptr) { return this_ptr->manager(); } -BDD BDD_Operator_Not(const BDD* this_ptr) { BDD bar = (! *this_ptr); return bar; }+void BDD_Operator_Not(BDD* ret_ptr, const BDD *this_ptr) { *ret_ptr = (!*this_ptr); } bool BDD_Operator_Equal(const BDD* this_ptr, const BDD* other) { bool b = (*this_ptr == *other); return b; } -BDD BDD_Operator_Or(const BDD* this_ptr, const BDD* other) { BDD bar = (*this_ptr + *other); return bar; }+void BDD_Operator_Or(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr + *other); } -BDD BDD_Operator_And(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr * *other); }+void BDD_Operator_And(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr * *other); } -BDD BDD_Operator_Xor(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr ^ *other); }+void BDD_Operator_Xor(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr ^ *other); } -BDD BDD_Operator_LessEqual(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr <= *other); }+void BDD_Operator_LessEqual(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr <= *other); } -BDD BDD_Operator_Nor(const BDD* this_ptr, const BDD* other) { return (BDD) (*this_ptr % *other); }+void BDD_Operator_Nor(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr % *other); } -BDD BDD_Operator_Nand(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr | *other); }+void BDD_Operator_Nand(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr | *other); } -BDD BDD_Operator_XNor(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr & *other); }+void BDD_Operator_XNor(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr & *other); } -void XBDDManager_ShowInfo(XBDDManager* this_ptr, double vtime) { return this_ptr->ShowInfo(); }+void XBDDManager_ShowInfo(XBDDManager* this_ptr) { this_ptr->ShowInfo(); }
c/BDDNodeC.h view
@@ -5,35 +5,37 @@ BDD* BDD_new(); const XManager* BDD_checkSameManager(const BDD* this_ptr, const BDD* other); int BDD_Variable(BDD* this_ptr);-BDD BDD_Then(const BDD* this_ptr);-BDD BDD_Else(const BDD* this_ptr);-BDD BDD_Exist(BDD* this_ptr, const BDD* cube);-BDD BDD_Universal(BDD* this_ptr, const BDD* cube);-BDD BDD_Restrict(const BDD* this_ptr, const BDD* other);-BDD BDD_Compose(const BDD* this_ptr, int v, const BDD* other);-BDD BDD_Permute(const BDD* this_ptr, const vector<int>* permu);-BDD BDD_AndExist(BDD* this_ptr, const BDD* other, const BDD* cube);+void BDD_Then(BDD* ret_ptr, const BDD* this_ptr);+void BDD_Else(BDD* ret_ptr, const BDD* this_ptr);+void BDD_Exist(BDD* ret_ptr, BDD* this_ptr, const BDD* cube);+void BDD_Universal(BDD* ret_ptr, BDD* this_ptr, const BDD* cube);+void BDD_Restrict(BDD* ret_ptr, const BDD* this_ptr, const BDD* other);+void BDD_Compose(BDD* ret_ptr, const BDD* this_ptr, int v, const BDD* other);+void BDD_Permute(BDD* ret_ptr, const BDD* this_ptr, const vector<int>* permu);+void BDD_AndExist(BDD* ret_ptr, BDD* this_ptr, const BDD* other, const BDD* cube); bool BDD_IsComp(BDD* this_ptr); const XManager* BDD_manager(const BDD* this_ptr); // In C we can not overload operators, so we use functions instead.-BDD BDD_Operator_Not (const BDD* this_ptr); // !+void BDD_Operator_Not (BDD* ret_ptr, const BDD* this_ptr); // !+ bool BDD_Operator_Equal (const BDD* this_ptr, const BDD* other); // ==-BDD BDD_Operator_Or (const BDD* this_ptr, const BDD* other); // +-BDD BDD_Operator_And (const BDD* this_ptr, const BDD* other); // *-BDD BDD_Operator_Xor (const BDD* this_ptr, const BDD* other); // ^-BDD BDD_Operator_LessEqual (const BDD* this_ptr, const BDD* other); // <=-BDD BDD_Operator_Nor (const BDD* this_ptr, const BDD* other); // %-BDD BDD_Operator_Nand (const BDD* this_ptr, const BDD* other); // |-BDD BDD_Operator_XNor (const BDD* this_ptr, const BDD* other); // &+void BDD_Operator_Or (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // ++void BDD_Operator_And (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // *+void BDD_Operator_Xor (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // ^+void BDD_Operator_LessEqual (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // <=+void BDD_Operator_Nor (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // %+void BDD_Operator_Nand (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // |+void BDD_Operator_XNor (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // & + XBDDManager* XBDDManager_new(int varCount);-BDD XBDDManager_BddOne(XBDDManager* this_ptr);-BDD XBDDManager_BddZero(XBDDManager* this_ptr);-BDD XBDDManager_BddVar(XBDDManager* this_ptr, int varIndex);-BDD XBDDManager_Ite(XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h);+void XBDDManager_BddOne(BDD* ret_ptr, XBDDManager* this_ptr);+void XBDDManager_BddZero(BDD* ret_ptr, XBDDManager* this_ptr);+void XBDDManager_BddVar(BDD* ret_ptr, XBDDManager* this_ptr, int varIndex);+void XBDDManager_Ite(BDD* ret_ptr, XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h); -void XBDDManager_ShowInfo(XBDDManager* this_ptr, double vtime);+void XBDDManager_ShowInfo(XBDDManager* this_ptr); const XManager* XBDDManager_manager(const XBDDManager* this_ptr); }
hs/Data/HasCacBDD.hs view
@@ -20,20 +20,23 @@ firstVarOf, maxVarOf, allVarsOf, allVarsOfSorted, -- * Sub-BDDs and length thenOf, elseOf, subsOf, sizeOf,+ -- * Variable Orderings+ optimalOrder, -- * Show and convert to trees BddTree(..), unravel, ravel, -- * Print some debugging information maximumvar, showInfo ) where -import Control.Arrow (Arrow(first)) import Foreign.C (CInt(..)) import Foreign.Ptr (Ptr) import Foreign (ForeignPtr, newForeignPtr, withForeignPtr, finalizerFree) import System.IO.Unsafe (unsafePerformIO)-import Data.List (nub,(\\),sort)-import Data.Maybe (fromJust)+import Data.Function (on)+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.@@ -52,16 +55,16 @@ type CacXBddManager = () newtype XBddManager = XBddManager (ForeignPtr CacXBddManager) -type NullOp = Ptr CacBDD -> Ptr CacXBddManager -> IO (Ptr CacBDD)-type UnaryOp = Ptr CacBDD -> Ptr CacBDD -> IO (Ptr CacBDD)-type BinaryOp = Ptr CacBDD -> Ptr CacBDD -> Ptr CacBDD -> IO (Ptr CacBDD)+type NullOp = Ptr CacBDD -> Ptr CacXBddManager -> IO ()+type UnaryOp = Ptr CacBDD -> Ptr CacBDD -> IO ()+type BinaryOp = Ptr CacBDD -> Ptr CacBDD -> Ptr CacBDD -> IO () -foreign import ccall unsafe "BDDNodeC.h BDD_new" bdd_new :: Word -> IO (Ptr CacBDD)+foreign import ccall unsafe "BDDNodeC.h BDD_new" bdd_new :: IO (Ptr CacBDD) foreign import ccall unsafe "BDDNodeC.h XBDDManager_new" xBddManager_new :: CInt -> IO (Ptr CacXBddManager) foreign import ccall unsafe "BDDNodeC.h XBDDManager_ShowInfo" xBddManager_showInfo :: Ptr CacXBddManager -> IO () foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddOne" xBddManager_BddOne :: NullOp foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddZero" xBddManager_BddZero :: NullOp-foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddVar" xBddManager_BddVar :: Ptr CacBDD -> Ptr CacXBddManager -> CInt -> IO (Ptr CacBDD)+foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddVar" xBddManager_BddVar :: Ptr CacBDD -> Ptr CacXBddManager -> CInt -> IO () foreign import ccall unsafe "BDDNodeC.h XBDDManager_Ite" xBddManager_Ite :: Ptr CacBDD -> Ptr CacXBddManager -> BinaryOp foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Equal" bdd_Operator_Equal :: Ptr CacBDD -> Ptr CacBDD -> IO Bool foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Not" bdd_Operator_Not :: UnaryOp@@ -85,19 +88,25 @@ fromManager :: NullOp -> Bdd fromManager nulloperator = let (XBddManager mptr) = manager in- finalize $ unsafePerformIO $- withForeignPtr mptr $ nulloperator (unsafePerformIO (bdd_new 8))+ finalize $ unsafePerformIO $ do+ b <- bdd_new+ withForeignPtr mptr $ nulloperator b+ return b {-# NOINLINE fromManager #-} withBDD :: UnaryOp -> Bdd -> Bdd-withBDD unioperator (Bdd fptr) = finalize $ unsafePerformIO $- withForeignPtr fptr $ unioperator (unsafePerformIO (bdd_new 8))+withBDD unioperator (Bdd fptr) = finalize $ unsafePerformIO $ do+ b <- bdd_new+ withForeignPtr fptr $ unioperator b+ return b {-# NOINLINE withBDD #-} withTwoBDDs :: BinaryOp -> Bdd -> Bdd -> Bdd-withTwoBDDs binoperator (Bdd fptr1) (Bdd fptr2) = finalize $ unsafePerformIO $+withTwoBDDs binoperator (Bdd fptr1) (Bdd fptr2) = finalize $ unsafePerformIO $ do+ b <- bdd_new withForeignPtr fptr1 $- withForeignPtr fptr2 . binoperator (unsafePerformIO (bdd_new 8))+ withForeignPtr fptr2 . binoperator b+ return b {-# NOINLINE withTwoBDDs #-} fromBDD :: (Ptr CacBDD -> IO a) -> Bdd -> a@@ -165,11 +174,13 @@ ifthenelse :: Bdd -> Bdd -> Bdd -> Bdd ifthenelse (Bdd test) (Bdd yes) (Bdd no) = let (XBddManager mptr) = manager in- finalize $ unsafePerformIO $+ finalize $ unsafePerformIO $ do+ b <- bdd_new withForeignPtr test (\t -> withForeignPtr yes (\y -> withForeignPtr no (\n ->- withForeignPtr mptr (\m -> xBddManager_Ite (unsafePerformIO (bdd_new 8)) m t y n))))+ withForeignPtr mptr (\m -> xBddManager_Ite b m t y n))))+ return b {-# NOINLINE ifthenelse #-} instance Eq Bdd where@@ -268,7 +279,7 @@ m1 = maxVarOf $ thenOf b m2 = maxVarOf $ elseOf b --- | All variables in a given BDD, *not* sorted, lazy.+-- | All variables in a given BDD, /not/ sorted, lazy. allVarsOf :: Bdd -> [Int] allVarsOf b | b == bot = []@@ -282,7 +293,7 @@ allVarsOfSorted = sort . allVarsOf -- | List all node / sub-BDDs of a given BDD.--- This includes the root node of b itself, but omits terminal nodes.+-- This includes the root node, but omits terminal nodes. subsOf :: Bdd -> [Bdd] subsOf = subsOf' [] where subsOf' done b@@ -297,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.@@ -358,20 +386,20 @@ -- | Given a set of all variables, complete an assignment. completeAss :: [Int] -> Assignment -> [Assignment] completeAss allvars ass =- if null (addvars ass)- then [ass]- else concatMap (completeAss allvars) (extend ass (head (addvars ass)))+ case addvars ass of+ [] -> [ass]+ n:_ -> concatMap (completeAss allvars) (extend ass n) where addvars s = allvars \\ sort (map fst s) extend s v = [ (v,False):s, (v,True):s ] --- | Get all complete assignments, given a set of all variables.+-- | Get all complete assignments, given a list of variables. -- In particular this will include variables not in the BDD. allSatsWith :: [Int] -> Bdd -> [Assignment] allSatsWith allvars b = concatMap (completeAss allvars) (allSats b) --- | Given a set of all variables, get the number of satisfying assignments.--- Note that allvars must be nub'd and sorted.+-- | Get the number of satisfying assignments, given a list of variables.+-- Note that the given list must be nub'd and sorted. satCountWith :: [Int] -> Bdd -> Int satCountWith allvars b | b == top = 2 ^ length allvars@@ -387,7 +415,7 @@ anySatWith :: [Int] -> Bdd -> Maybe Assignment anySatWith allvars b = case anySat b of Nothing -> Nothing- Just partass -> Just $ head $ completeAss allvars partass+ Just partass -> listToMaybe $ completeAss allvars partass -- | Relabel variables according to the given mapping. -- Note that the mapping list must be sorted!@@ -427,6 +455,12 @@ Just k -> case lookup k repls of Nothing -> ifthenelse (var k) (substitSimul repls $ thenOf b) (substitSimul repls $ elseOf b) Just psi -> ifthenelse psi (substitSimul repls $ thenOf b) (substitSimul repls $ elseOf b)++-- | Find an optimal variable-reording.+-- Returns a relabelling @r@ such that @sizeOf (relabel r b)@ is minimal.+optimalOrder :: Bdd -> [(Int,Int)]+optimalOrder b = minimumBy (compare `on` (\r -> sizeOf (relabel r b))) allPermut where+ allPermut = map (zip (allVarsOf b)) $ permutations (allVarsOf b) -- | Show internal statistics. showInfo :: IO ()
hs/Data/HasCacBDD/Visuals.hs view
@@ -1,13 +1,16 @@--- | Very simple visualisation of BDDs using /dot/.+-- | Visualisation of BDDs using the @dot@ program from [GraphViz](https://graphviz.org/). module Data.HasCacBDD.Visuals ( genGraph, genGraphWith, showGraph,- svgGraph+ svgGraph,+ svgGraphWithPath, ) where +import Control.Monad (filterM) import Data.Maybe (fromJust)+import System.Directory (doesFileExist) import System.Exit import System.IO import System.Process@@ -51,7 +54,8 @@ rankings = concat [ "{ rank=same; "++ unwords (nodesOf v) ++ " }\n" | v <- allVarsOf myb ] nodesOf v = map (("n"++).show.snd) $ filter ( \(b,_) -> firstVarOf b == Just v ) topdone --- | Display the graph of a BDD with dot.+-- | Display the graph of a BDD with @\/usr\/bin\/dot -Tx11@.+-- Only works on Linux. On other systems consider using 'svgGraph'. showGraph :: Bdd -> IO () showGraph b = do (inp,_,_,pid) <- runInteractiveProcess "/usr/bin/dot" ["-Tx11"] Nothing Nothing@@ -61,10 +65,32 @@ _ <- waitForProcess pid return () --- | Generate SVG of a BDD with dot.-svgGraph :: Bdd -> IO String-svgGraph b = do- (exitCode,out,err) <- readProcessWithExitCode "/usr/bin/dot" ["-Tsvg" ] (genGraph b)+-- | Generate SVG of a BDD with the @dot@ executable installed at the given path.+svgGraphWithPath :: String -> Bdd -> IO String+svgGraphWithPath dot b = do+ (exitCode,out,err) <- readProcessWithExitCode dot ["-Tsvg" ] (genGraph b) case exitCode of- ExitSuccess -> return $ (unlines.tail.lines) out+ ExitSuccess -> case lines out of+ [] -> error "dot -Tsvg succeeded but did not provide any output."+ _:rest -> return (unlines rest)+ -- NOTE: we remove the first line of the output which is+ -- "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n" ExitFailure n -> error $ "dot -Tsvg failed with exit code " ++ show n ++ " and error: " ++ err++-- | Generate SVG of a BDD, trying default locations to find @dot@.+svgGraph :: Bdd -> IO String+svgGraph b = findDotPath >>= \ dot -> svgGraphWithPath dot b++-- | Try to find the @dot@ executable at some default locations.+-- Results in an error when the exectuable is not found.+findDotPath :: IO FilePath+findDotPath =+ let dotPaths = [ "/usr/bin/dot"+ , "/opt/homebrew/bin/dot"+ , "C:\\Program Files\\Graphviz\\bin\\dot.exe"+ , "C:\\Program Files (x86)\\Graphviz\\bin\\dot.exe" ]+ in do+ results <- filterM doesFileExist dotPaths+ case results of+ dot:_ -> return dot+ [] -> error "Cound not find 'dot' at a standard path. Please use svgGraphWithPath instead."
stack.yaml view
@@ -1,3 +1,3 @@-resolver: lts-21.19+resolver: lts-23.27 packages: - '.'
tests/Main.hs view
@@ -1,22 +1,26 @@-module Main where+{-# OPTIONS_GHC -Wno-x-partial #-} -import Data.HasCacBDD-import Data.List (nub)+module Main (main) where++import Data.List ((\\),nub) import Data.Maybe (fromJust,isNothing) import Data.Tuple (swap) import Test.QuickCheck import Test.Hspec import Test.Hspec.QuickCheck +import Data.HasCacBDD+import Data.HasCacBDD.Visuals+ 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@@ -63,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)@@ -86,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 ))@@ -116,16 +118,60 @@ 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 "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 "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)+ 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) prop "wrong deMorganOne" $ expectFailure (\a b -> neg (a `con` b) === (neg a `con` neg b)) prop "wrong deMorganTwo" $ expectFailure (\a b -> neg (a `dis` b) === (neg a `dis` neg b)) modifyMaxSuccess (* 1000) $ prop "folding substit is not the same as substitSimul" $ expectFailure (\b1 b2 c -> foldl (flip $ uncurry substit) c [(1,b1),(2,b2)] === substitSimul [(1,b1),(2,b2)] c)+ describe "Visualisation" $ do+ describe "genGraph" $ do+ it "var 12345" $ genGraph (var 12345) `shouldContain` "12345"+ it "top has no circles" $ genGraph top `shouldNotContain` "circle"+ it "bot had no circles" $ genGraph bot `shouldNotContain` "circle"+ it "bot /= top" $ genGraph bot /= genGraph top+ describe "svgGraph" $ do+ it "svgGraph top returns an svg" $+ (svgGraph top >>= \ s -> return (take 13 s == "<!DOCTYPE svg")) `shouldReturn` True+ it "svgGraph top is short" $+ (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)