diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,8 +1,9 @@ # HasCacBDD Changelog -## upcoming +## 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) diff --git a/HasCacBDD.cabal b/HasCacBDD.cabal --- a/HasCacBDD.cabal +++ b/HasCacBDD.cabal @@ -1,5 +1,5 @@ name: HasCacBDD -version: 0.3.0.0 +version: 0.3.0.1 synopsis: Haskell bindings for CacBDD homepage: https://github.com/m4lvin/HasCacBDD license: GPL-2 @@ -42,7 +42,8 @@ Data.HasCacBDD.Visuals build-depends: base >=4.8 && < 5, 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 diff --git a/hs/Data/HasCacBDD.hs b/hs/Data/HasCacBDD.hs --- a/hs/Data/HasCacBDD.hs +++ b/hs/Data/HasCacBDD.hs @@ -35,7 +35,7 @@ import System.IO.Unsafe (unsafePerformIO) import Data.Function (on) import Data.List ((\\), minimumBy, nub, permutations, sort) -import Data.Maybe (fromJust) +import Data.Maybe (fromJust, listToMaybe) import Test.QuickCheck (Arbitrary, Gen, arbitrary, shrink, choose, oneof, sized, listOf) -- | The CacBDD datatype has no structure because @@ -369,9 +369,9 @@ -- | 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 ] @@ -398,7 +398,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! diff --git a/hs/Data/HasCacBDD/Visuals.hs b/hs/Data/HasCacBDD/Visuals.hs --- a/hs/Data/HasCacBDD/Visuals.hs +++ b/hs/Data/HasCacBDD/Visuals.hs @@ -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 + -- "\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." diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -1,3 +1,3 @@ -resolver: lts-21.25 +resolver: lts-23.27 packages: - '.' diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,6 +1,7 @@ +{-# OPTIONS_GHC -Wno-x-partial #-} + module Main where -import Data.HasCacBDD import Data.List ((\\),nub) import Data.Maybe (fromJust,isNothing) import Data.Tuple (swap) @@ -8,6 +9,9 @@ import Test.Hspec import Test.Hspec.QuickCheck +import Data.HasCacBDD +import Data.HasCacBDD.Visuals + main :: IO () main = hspec $ do describe "Examples" $ do @@ -135,3 +139,16 @@ 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 == ">= \ s -> return (length s < 1000)) `shouldReturn` True + it "svgGraph (var 1) is longer" $ + (svgGraph (var 1) >>= \ s -> return (length s > 1000)) `shouldReturn` True