HasCacBDD 0.1.0.4 → 0.2.0.0

raw patch · 7 files changed

+79/−32 lines, 7 filesdep ~QuickCheckdep ~hspecdep ~processPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: QuickCheck, hspec, process

API changes (from Hackage documentation)

Files

• CHANGELOG.md +37/−0
• HasCacBDD.cabal +7/−4
• README.md +5/−1
• hs/Data/HasCacBDD.hs +20/−18
• hs/Data/HasCacBDD/Visuals.hs +4/−3
• stack.yaml +1/−1
• tests/Main.hs +5/−5

@@ -0,0 +1,37 @@+# HasCacBDD Changelog++## upcoming++- ...++## v0.2.0.0 (2023-11-23)++- rename `forall` (soon a keyword in GHC) to `forall_` and `exists` to `exists_`++## v0.1.0.4 (2023-02-03)++Maintenance release.++- Faster subsOf and sizeOf.++## v0.1.0.3 (2020-06-30)++Maintenance release.++- fix an error which caused `svgGraph` to hang on long outputs.+- add `Read` and `Eq` classes for BddTree.+- a few more tests.++## v0.1.0.2 (2019-06-19)++Correction to extra library paths defined in custom `Setup.hs`. This should fix problems when HasCacBDD is used as a dependency in projects with recent stack versions.++## v0.1.0.1 (2019-01-24)++- new functions: `relabelFun`, `substit`, `substitSimul`+- simplified test suite+- improve documentation and hints to get started++## v0.1.0.0 (2017-03-09)++First complete release, also available on hackage.

@@ -1,5 +1,5 @@ name:                HasCacBDD-version:             0.1.0.4+version:             0.2.0.0 synopsis:            Haskell bindings for CacBDD homepage:            https://github.com/m4lvin/HasCacBDD license:             GPL-2@@ -25,6 +25,9 @@   cpp/OriginalMakefile   cpp/README +extra-doc-files:+  CHANGELOG.md+ source-repository head   type:     git   location: git://github.com/m4lvin/HasCacBDD.git@@ -38,8 +41,8 @@   exposed-modules:     Data.HasCacBDD,                        Data.HasCacBDD.Visuals   build-depends:       base >=4.8 && < 5,-                       process >= 1.1,-                       QuickCheck+                       process >= 1.1 && < 1.7,+                       QuickCheck >= 2.4 && < 2.15   default-language:    Haskell2010   hs-source-dirs:      hs   extra-libraries:     stdc++, CacBDD@@ -53,6 +56,6 @@   hs-source-dirs:      tests   build-depends:       base >=4.8,                        HasCacBDD,-                       hspec,+                       hspec < 2.12,                        QuickCheck > 2.4   ghc-options:         -Wall -threaded

@@ -3,6 +3,8 @@  [![Release](https://img.shields.io/github/release/m4lvin/HasCacBDD.svg)](https://github.com/m4lvin/HasCacBDD/releases) [![Hackage](https://img.shields.io/hackage/v/HasCacBDD.svg)](https://hackage.haskell.org/package/HasCacBDD)+[![GitLab CI](https://gitlab.com/m4lvin/HasCacBDD/badges/master/pipeline.svg)](https://gitlab.com/m4lvin/HasCacBDD/-/pipelines)+[![Test Coverage](https://gitlab.com/m4lvin/HasCacBDD/badges/master/coverage.svg)](https://gitlab.com/m4lvin/HasCacBDD/-/jobs/artifacts/master/file/hpc/combined/all/hpc_index.html?job=test)  Haskell bindings for CacBDD, a Binary Decision Diagram (BDD) package with dynamic cache management. @@ -27,7 +29,9 @@     Note: `stack ghci` apparently does not work with the shared library.     You really need `stack build` and then `stack exec ghci`. -3. Play :-)+    To use cabal instead of stack: `cabal build`, then `cabal exec ghci` and then `:set -package HasCacBDD`.++3. Now you can play with Boolean functions :-)         λ> import Data.HasCacBDD        λ> var 5

@@ -8,7 +8,7 @@   top, bot, var,   -- * Combination and Manipulation of BDDs   neg, con, dis, imp, equ, xor, conSet, disSet, xorSet,-  exists, forall, forallSet, existsSet,+  exists_, forall_, existsSet, forallSet,   restrict, restrictSet, restrictLaw,   ifthenelse, gfp, relabel, relabelFun,   substit, substitSimul,@@ -127,22 +127,22 @@ {-# NOINLINE restrictLaw #-}  -- | Existential Quantification-exists :: Int -> Bdd -> Bdd-exists n b = withTwoBDDs bdd_Exist b (var n)-{-# NOINLINE exists #-}+exists_ :: Int -> Bdd -> Bdd+exists_ n b = withTwoBDDs bdd_Exist b (var n)+{-# NOINLINE exists_ #-}  -- | Universal Quantification-forall :: Int -> Bdd -> Bdd-forall n b = withTwoBDDs bdd_Universal b (var n)-{-# NOINLINE forall #-}+forall_ :: Int -> Bdd -> Bdd+forall_ n b = withTwoBDDs bdd_Universal b (var n)+{-# NOINLINE forall_ #-}  -- | Big Existential Quantification existsSet :: [Int] -> Bdd -> Bdd-existsSet ns b = foldl (flip exists) b ns+existsSet ns b = foldl (flip exists_) b ns  -- | Big Universal Quantification forallSet :: [Int] -> Bdd -> Bdd-forallSet ns b = foldl (flip forall) b ns+forallSet ns b = foldl (flip forall_) b ns  -- | True constant top :: Bdd@@ -273,7 +273,9 @@ allVarsOf b   | b == bot = []   | b == top = []-  | otherwise = let (Just n) = firstVarOf b in n : nub (allVarsOf (thenOf b) ++ allVarsOf (elseOf b))+  | otherwise =+      let n = fromJust (firstVarOf b)+      in n : nub (allVarsOf (thenOf b) ++ allVarsOf (elseOf b))  -- | All variables in a given BDD, sorted, *not* lazy. allVarsOfSorted :: Bdd -> [Int]@@ -308,7 +310,7 @@ unravel b   | b == bot = Bot   | b == top = Top-  | otherwise = Var n (unravel (thenOf b)) (unravel (elseOf b)) where (Just n) = firstVarOf b+  | otherwise = Var n (unravel (thenOf b)) (unravel (elseOf b)) where n = fromJust $ firstVarOf b  -- | Convert a tree to a BDD. ravel :: BddTree -> Bdd@@ -330,7 +332,7 @@   | b == bot = False   | b == top = True   | otherwise =-      let (Just n) = firstVarOf b+      let n = fromJust $ firstVarOf b       in evaluateFun ((if f n then thenOf else elseOf) b) f  -- | Get all satisfying assignments. These will be partial, i.e. only@@ -341,7 +343,7 @@   | b == top = [ [] ]   | otherwise =       [ (n,True):rest | rest <- allSats (thenOf b) ] ++ [ (n,False):rest | rest <- allSats (elseOf b) ]-      where (Just n) = firstVarOf b+      where n = fromJust $ firstVarOf b  -- | Get the lexicographically smallest satisfying assignment, if there is any. anySat :: Bdd -> Maybe Assignment@@ -350,8 +352,8 @@   | b == top = Just []   | otherwise = Just ((n,hastobetrue):rest) where       hastobetrue = elseOf b == bot-      (Just n)    = firstVarOf b-      (Just rest) = if hastobetrue then anySat (thenOf b) else anySat (elseOf b)+      n = fromJust $ firstVarOf b+      rest = fromJust $ if hastobetrue then anySat (thenOf b) else anySat (elseOf b)  -- | Given a set of all variables, complete an assignment. completeAss :: [Int] -> Assignment -> [Assignment]@@ -375,7 +377,7 @@   | b == top = 2 ^ length allvars   | b == bot = 0   | otherwise = (2 ^ length varsjumped) * posbelow where-      (Just curvar) = firstVarOf b+      curvar = fromJust $ firstVarOf b       varsjumped = filter (< curvar) allvars       varsleft   = filter (> curvar) allvars       posbelow   = sum [satCountWith varsleft (branch b) | branch <- [thenOf,elseOf] ]@@ -454,9 +456,9 @@   , imp <$> smallerbdd <*> smallerbdd   , equ <$> smallerbdd <*> smallerbdd   , xor <$> smallerbdd <*> smallerbdd-  , exists <$> randomvarnumber <*> smallerbdd+  , exists_ <$> randomvarnumber <*> smallerbdd   , existsSet <$> listOf randomvarnumber <*> smallerbdd-  , forall <$> randomvarnumber <*> smallerbdd+  , forall_ <$> randomvarnumber <*> smallerbdd   , forallSet <$> listOf randomvarnumber <*> smallerbdd   ]   where

@@ -7,6 +7,7 @@   svgGraph ) where +import Data.Maybe (fromJust) import System.Exit import System.IO import System.Process@@ -30,17 +31,17 @@             let               thisn = if null done then 0 else maximum (map snd done) + 1               thisnstr = show thisn-              (Just thisvar) = firstVarOf curB+              thisvar = fromJust $ firstVarOf curB               out1  = "n" ++ thisnstr ++ " [label=\"" ++ myShow thisvar ++ "\",shape=\"circle\"];\n"               (lhs, rhs) = (thenOf curB, elseOf curB)               (lhsoutput,lhsdone) = genGraphStep ((curB,thisn):done) lhs-              (Just leftn) = lookup lhs lhsdone+              leftn = fromJust $ lookup lhs lhsdone               out2                 | lhs == top = "n"++ thisnstr ++" -> Top;\n"                 | lhs == bot = "n"++ thisnstr ++" -> Bot;\n"                 | otherwise  = "n"++ thisnstr ++" -> n" ++ show leftn ++";\n" ++ lhsoutput               (rhsoutput,rhsdone) = genGraphStep lhsdone rhs-              (Just rightn) = lookup rhs rhsdone+              rightn = fromJust $ lookup rhs rhsdone               out3                 | rhs == top = "n"++ thisnstr ++" -> Top [style=dashed];\n"                 | rhs == bot = "n"++ thisnstr ++" -> Bot [style=dashed];\n"

@@ -1,3 +1,3 @@-resolver: lts-18.21+resolver: lts-21.19 packages: - '.'

@@ -23,7 +23,7 @@       it "var 1 == var 1" $ var 1 `shouldBe` var 1       it "imp (var 1) (var 1) == top" $ imp (var 1) (var 1) `shouldBe` top       it "equ (var 1) (var 1) == top" $ equ (var 1) (var 1) `shouldBe` top-      it "exists 1 (neg $ var 1) == top" $ exists 1 (neg $ var 1) `shouldBe` top+      it "exists_ 1 (neg $ var 1) == top" $ exists_ 1 (neg $ var 1) `shouldBe` top       it "gfp (\b -> con b (var 3)) == var 3" $ gfp (\b -> con b (var 3)) `shouldBe` var 3       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@@ -35,7 +35,7 @@       it "dis (var 1) (neg $ var 2) /= top" $ dis (var 1) (neg $ var 2) `shouldNotBe` top       it "dis (var 1) (var 2) /= top" $ dis (var 1) (var 2) `shouldNotBe` top       it "var 1 /= var 2" $ var 1 `shouldNotBe` var 2-      it "forall 1 (var 1) /= top" $ forall 1 (var 1) `shouldNotBe` top+      it "forall_ 1 (var 1) /= top" $ forall_ 1 (var 1) `shouldNotBe` top     describe "Laws from de Morgan:" $ do       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))@@ -57,8 +57,8 @@     it "var 3 == con (var 3) top" $ var 3 `shouldBe` con (var 3) top     it "var 4 /= con (var 3) top" $ var 4 `shouldNotBe` con (var 3) top     it "equ (var 1) (var 1) == top" $ equ (var 1) (var 1) `shouldBe` top-    it "exists 1 (neg $ var 1) == top" $ exists 1 (neg $ var 1) `shouldBe` top-    it "exists 1 (neg $ var 2) /= top" $ exists 1 (neg $ var 2) `shouldNotBe` top+    it "exists_ 1 (neg $ var 1) == top" $ exists_ 1 (neg $ var 1) `shouldBe` top+    it "exists_ 1 (neg $ var 2) /= top" $ exists_ 1 (neg $ var 2) `shouldNotBe` top     it "gfp (\b -> con b (var 3)) == var 3" $ gfp (\b -> con b (var 3)) `shouldBe` var 3     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@@ -82,7 +82,7 @@     prop "conElim"        (\a b -> imp (con a b) a == top)     prop "conElim3"       (\a b c -> imp (conSet [a, b, c]) a == top)     prop "negNotEqual"    (\b -> neg b /= b)-    prop "quantifDuality" (forAll (elements [0..maximumvar]) (\n b -> forall n b == neg (exists n (neg b))))+    prop "quantifDuality" (forAll (elements [0..maximumvar]) (\n b -> forall_ n b == neg (exists_ n (neg b))))     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))))