HasCacBDD 0.1.0.0 → 0.1.0.1
raw patch · 9 files changed
+202/−188 lines, 9 filesdep +hspecdep ~basePVP: minor bump suggested
API additions: PVP suggests at least a minor version bump
Dependencies added: hspec
Dependency ranges changed: base
API changes (from Hackage documentation)
+ Data.HasCacBDD: relabelFun :: (Int -> Int) -> Bdd -> Bdd
+ Data.HasCacBDD: substit :: Int -> Bdd -> Bdd -> Bdd
+ Data.HasCacBDD: substitSimul :: [(Int, Bdd)] -> Bdd -> Bdd
Files
- HasCacBDD.cabal +6/−23
- README.md +31/−0
- hs/Data/HasCacBDD.hs +37/−7
- hs/Data/HasCacBDD/Visuals.hs +3/−6
- stack.yaml +1/−1
- tests/Basics.hs +0/−44
- tests/Example.hs +0/−44
- tests/Main.hs +124/−0
- tests/Tautologies.hs +0/−63
HasCacBDD.cabal view
@@ -1,5 +1,5 @@ name: HasCacBDD-version: 0.1.0.0+version: 0.1.0.1 synopsis: Haskell bindings for CacBDD homepage: https://github.com/m4lvin/HasCacBDD license: GPL-2@@ -8,7 +8,7 @@ maintainer: malvin@w4eg.de category: Data build-type: Custom-cabal-version: >=1.23+cabal-version: 1.24 description: Haskell bindings for CacBDD, a Binary Decision Diagram (BDD) package with dynamic cache management. Original C++ code from <http://kailesu.net/CacBDD> and a C wrapper are included.@@ -46,30 +46,13 @@ cc-options: -fPIC -shared ghc-options: -pgml g++ -Wall -fPIC -fno-full-laziness -test-suite example- default-language: Haskell2010- type: exitcode-stdio-1.0- main-is: Example.hs- hs-source-dirs: tests- build-depends: base >=4.8,- HasCacBDD- ghc-options: -pgml g++ -Wall -fPIC -fno-full-laziness--test-suite basics- default-language: Haskell2010- type: exitcode-stdio-1.0- main-is: Basics.hs- hs-source-dirs: tests- build-depends: base >=4.8,- HasCacBDD- ghc-options: -Wall--test-suite tautologies+test-suite tests default-language: Haskell2010 type: exitcode-stdio-1.0- main-is: Tautologies.hs+ main-is: Main.hs hs-source-dirs: tests build-depends: base >=4.8, HasCacBDD,+ hspec, QuickCheck > 2.4- ghc-options: -Wall -fhpc -fforce-recomp+ ghc-options: -Wall -threaded
README.md view
@@ -1,8 +1,39 @@ HasCacBDD ========= +[](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. Original C++ code from <http://kailesu.net/CacBDD> and a C wrapper are included.+++# Getting Started++1. Install C compilers and stack if necessary:++ apt install build-essential git+ curl -sSL https://get.haskellstack.org/ | sh++2. Download, build and load the lastest version:++ git clone https://github.com/m4lvin/HasCacBDD.git+ cd HasCacBDD+ stack setup+ stack build+ stack exec ghci++ Note: `stack ghci` apparently does not work with the shared library.+ You really need `stack build` and then `stack exec ghci`.++3. Play :-)++ λ> import Data.HasCacBDD+ λ> var 5+ Var 5 Top Bot+ λ> neg (var 5)+ Var 5 Bot Top+ λ> dis (neg (var 3)) (var 3)+ Top
hs/Data/HasCacBDD.hs view
@@ -10,7 +10,8 @@ neg, con, dis, imp, equ, xor, conSet, disSet, xorSet, exists, forall, forallSet, existsSet, restrict, restrictSet, restrictLaw,- ifthenelse, gfp, relabel,+ ifthenelse, gfp, relabel, relabelFun,+ substit, substitSimul, -- * Evaluation evaluate, evaluateFun, -- * Get satisfying assignments@@ -31,7 +32,7 @@ import System.IO.Unsafe import Data.List (nub,(\\),sort) import Data.Maybe (fromJust)-import Test.QuickCheck (Arbitrary, Gen, arbitrary, choose, oneof, sized, listOf)+import Test.QuickCheck (Arbitrary, Gen, arbitrary, shrink, choose, oneof, sized, listOf) -- | The CacBDD datatype has no structure because -- from our perspective BDDs are just pointers.@@ -41,7 +42,6 @@ -- | An assignment of boolean values to variables/integers. type Assignment = [(Int,Bool)] --- | We attach the free() finalizer to our BDDs. finalize :: Ptr CacBDD -> Bdd finalize ptr = Bdd (unsafePerformIO $ newForeignPtr finalizerFree ptr) @@ -82,7 +82,6 @@ manager = finalizeMgr (unsafePerformIO $ xBddManager_new (fromIntegral maximumvar)) {-# NOINLINE manager #-} --- | This should cover BDDOne, BddZero fromManager :: NullOp -> Bdd fromManager nulloperator = let (XBddManager mptr) = manager in finalize $ unsafePerformIO $@@ -121,7 +120,7 @@ restrictSet b bits = withTwoBDDs bdd_Restrict b (conSet $ map (\(n,bit) -> if bit then var n else neg (var n)) bits) {-# NOINLINE restrictSet #-} --- | Restrict with a law+-- | Restrict with a law. Note that the law is the second parameter! restrictLaw :: Bdd -> Bdd -> Bdd restrictLaw = withTwoBDDs bdd_Restrict {-# NOINLINE restrictLaw #-}@@ -365,7 +364,7 @@ allSatsWith allvars b = concatMap (completeAss allvars) (allSats b) -- | Given a set of all variables, get the number of satisfying assignments.--- Note that allvars should be nub'd and sorted.+-- Note that allvars must be nub'd and sorted. satCountWith :: [Int] -> Bdd -> Int satCountWith allvars b | b == top = 2 ^ length allvars@@ -384,6 +383,7 @@ Just partass -> Just $ head $ completeAss allvars partass -- | Relabel variables according to the given mapping.+-- Note that the mapping list must be sorted! relabel :: [(Int,Int)] -> Bdd -> Bdd relabel [] b = b relabel rel@((n,newn):rest) b@@ -394,6 +394,33 @@ EQ -> ifthenelse (var newn) (relabel rest (thenOf b)) (relabel rest (elseOf b)) GT -> ifthenelse (var (fromJust (firstVarOf b))) (relabel rel (thenOf b)) (relabel rel (elseOf b)) +-- | Relabel variables according to the given function.+relabelFun :: (Int -> Int) -> Bdd -> Bdd+relabelFun f b = case firstVarOf b of+ Nothing -> b+ Just m -> ifthenelse (var (f m)) (relabelFun f (thenOf b)) (relabelFun f (elseOf b))++-- | Substitute a BDD for a given variable in another BDD.+substit :: Int -> Bdd -> Bdd -> Bdd+substit n psi b =+ case firstVarOf b of+ Nothing -> b+ Just k -> case compare n k of+ LT -> b+ EQ -> ifthenelse psi (thenOf b) (elseOf b)+ GT -> ifthenelse (var k) (substit n psi (thenOf b)) (substit n psi (elseOf b))++-- | Simultaneous substitution of BDDs for variables.+-- Note that this is not the same as folding `substit`.+substitSimul :: [(Int,Bdd)] -> Bdd -> Bdd+substitSimul [] b = b+substitSimul repls b =+ case firstVarOf b of+ Nothing -> b+ 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)+ -- | Show internal statistics. showInfo :: IO () showInfo = withForeignPtr mptr xBddManager_showInfo where (XBddManager mptr) = manager@@ -401,6 +428,9 @@ -- | QuickCheck Arbitrary instances for BDDs instance Arbitrary Bdd where arbitrary = sized randombdd+ shrink b | b == top = []+ | b == bot = []+ | otherwise = [thenOf b, elseOf b] randomvarnumber :: Gen Int randomvarnumber = choose (0, 100)@@ -425,4 +455,4 @@ , forallSet <$> listOf randomvarnumber <*> smallerbdd ] where- smallerbdd = randombdd (min (n `div` 2) 10)+ smallerbdd = randombdd (n `div` 2)
hs/Data/HasCacBDD/Visuals.hs view
@@ -23,23 +23,20 @@ | otherwise = "strict digraph g {\n" ++ links ++ sinks ++ rankings ++ "}" where (links,topdone) = genGraphStep [] myb genGraphStep :: [(Bdd,Int)] -> Bdd -> (String,[(Bdd,Int)])- genGraphStep done curB = case (lookup curB done, curB == top || curB == bot) of- (_ ,True) -> ("",done)- (Just _, _) -> ("",done)- (Nothing,False) ->+ genGraphStep done curB =+ if curB `elem` [top,bot] ++ map fst done then ("",done) else let thisn = if null done then 0 else maximum (map snd done) + 1 thisnstr = show thisn (Just thisvar) = firstVarOf curB out1 = "n" ++ thisnstr ++ " [label=\"" ++ myShow thisvar ++ "\",shape=\"circle\"];\n"- lhs = thenOf curB+ (lhs, rhs) = (thenOf curB, elseOf curB) (lhsoutput,lhsdone) = genGraphStep ((curB,thisn):done) lhs (Just leftn) = lookup lhs lhsdone out2 | lhs == top = "n"++ thisnstr ++" -> Top;\n" | lhs == bot = "n"++ thisnstr ++" -> Bot;\n" | otherwise = "n"++ thisnstr ++" -> n" ++ show leftn ++";\n" ++ lhsoutput- rhs = elseOf curB (rhsoutput,rhsdone) = genGraphStep lhsdone rhs (Just rightn) = lookup rhs rhsdone out3
stack.yaml view
@@ -1,3 +1,3 @@-resolver: lts-8.0+resolver: lts-12.9 packages: - '.'
− tests/Basics.hs
@@ -1,44 +0,0 @@-module Main where--import Data.HasCacBDD-import System.Exit--main :: IO ()-main = do- putStrLn "\nRunning basic tests ..."- if all snd tests- then do- putStrLn "All passed."- exitSuccess- else do- putStrLn "FAILURES:"- let failures = filter (not.snd) tests- mapM_ (putStrLn . fst) failures- putStrLn "All results:"- mapM_ print tests- exitFailure--tests :: [(String,Bool)]-tests =- [ ("top == top", top == top)- , ("top /= bot", top /= bot)- , ("bot /= top", bot /= top)- , ("bot == bot", bot == bot)- , ("neg bot == top", neg bot == top)- , ("neg bot /= bot", neg bot /= bot)- , ("var 1 == var 1", var 1 == var 1)- , ("var 5 /= var 7", var 5 /= var 7)- , ("null (allSats bot)", null (allSats bot))- , ("allSats top == [[]]", allSats top == [[]])- , ("var 3 == con (var 3) top", var 3 == con (var 3) top)- , ("var 4 /= con (var 3) top", var 4 /= con (var 3) top)- , ("equ (var 1) (var 1) == top", equ (var 1) (var 1) == top)- , ("exists 1 (neg $ var 1) == top", exists 1 (neg $ var 1) == top)- , ("exists 1 (neg $ var 2) /= top", exists 1 (neg $ var 2) /= top)- , ("gfp (\b -> con b (var 3)) == var 3", gfp (\b -> con b (var 3)) == var 3)- , ("imp (conSet [var 1, var 0]) (var 1) == top", imp (conSet [var 1, var 0]) (var 1) == top)- , ("imp (conSet [var 0, var 1]) (var 0) == top", imp (conSet [var 0, var 1]) (var 0) == top)- , ("imp (con (var 0) (var 1)) (var 0) == top", imp (con (var 0) (var 1)) (var 0) == top)- , ("show top == \"Top\"", show top == "Top")- , ("show bot == \"Bot\"", show bot == "Bot")- ]
− tests/Example.hs
@@ -1,44 +0,0 @@-module Main-where--import Data.HasCacBDD-import System.Exit-import System.IO--main :: IO ()-main = do- hSetBuffering stdout NoBuffering- putStrLn "Creating some BDDs:"- putStrLn $ "top : " ++ show top- putStrLn $ "bot : " ++ show bot- putStrLn $ "var1: " ++ show (var 1)- putStrLn $ "var1: " ++ show (var 1)- putStrLn $ "var2: " ++ show (var 2)- putStrLn "\nChecking some tautologies:"- print $ bot == bot- print $ top == top- print $ var 1 == var 1- print $ imp (var 1) (var 1) == top- print $ equ (var 1) (var 1) == top- print $ exists 1 (neg $ var 1) == top- print $ gfp (\b -> con b (var 3)) == var 3- print $ imp (conSet [var 1, var 0]) (var 1) == top- print $ imp (conSet [var 0, var 1]) (var 0) == top- print $ imp (con (var 0) (var 1)) (var 0) == top- putStrLn "\nAnd some contradictions:"- print $ bot == top- print $ top == bot- print $ var 1 == top- print $ dis (var 1) (neg $ var 2) == top- print $ dis (var 1) (var 2) == top- print $ var 1 == var 2- print $ forall 1 (var 1) == top- putStrLn "\nLaws from de Morgan:"- print $ dis (neg $ var 1) (neg $ var 2) == neg (con (var 1) (var 2))- print $ con (neg $ var 1) (neg $ var 2) == neg (dis (var 1) (var 2))- putStrLn "\nThe example from CacBDDs main.cpp: (!x[4] + !x[6]) * (!x[3] + !x[6]) * (!x[2] + !x[5])"- let cacExample = conSet [ dis (neg (var 4)) (neg (var 6)) , neg (var 3) `dis` neg (var 6), neg (var 2) `dis` neg (var 5) ]- print cacExample- print $ cacExample == top- putStrLn "Good Bye."- exitSuccess
+ tests/Main.hs view
@@ -0,0 +1,124 @@+module Main where++import Data.HasCacBDD+import Data.List (nub)+import Data.Maybe (fromJust,isNothing)+import Data.Tuple (swap)+import Test.QuickCheck+import Test.Hspec+import Test.Hspec.QuickCheck++main :: IO ()+main = hspec $ do+ 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"+ describe "Some tautologies" $ do+ it "bot == bot" $ bot `shouldBe` bot+ it "top == top" $ top `shouldBe` top+ 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 "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+ it "imp (con (var 0) (var 1)) (var 0) == top" $ imp (con (var 0) (var 1)) (var 0) `shouldBe` top+ describe "Some non-tautologies" $ do+ it "bot /= top" $ bot `shouldNotBe` top+ it "top /= bot" $ top `shouldNotBe` bot+ it "var 1 /= top" $ var 1 `shouldNotBe` top+ 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+ 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 "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" $+ showInfo `shouldReturn` ()+ describe "Basics" $ do+ it "top == top" $ top `shouldBe` top+ it "top /= bot" $ top `shouldNotBe` bot+ it "bo /= 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+ it "var 1 == var 1" $ var 1 `shouldBe` var 1+ it "var 5 == var 7" $ var 5 `shouldNotBe` var 7+ it "null (allSats bot)" $ null (allSats bot)+ it "allSats top `==` [[]]" $ allSats top `shouldBe` [[]]+ 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 "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+ 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"+ describe "QuickCheck Properties" $ do+ prop "selfEqual" (\b -> (b::Bdd) == b)+ prop "idSymmetry" (\a b -> ((a::Bdd) == (b::Bdd)) == (b == a))+ prop "singleNegation" (\b -> neg b /= b)+ prop "doubleNegation" (\b -> neg (neg b) == b)+ prop "selfImp" (\b -> imp b b == top)+ prop "selfEqu" (\b -> equ b b == top)+ prop "selfXor" (\b -> xor b b == bot)+ prop "excludedMiddle" (\b -> b `dis` neg b == top)+ prop "deMorganOne" (\a b -> neg (a `con` b) == (neg a `dis` neg b))+ prop "deMorganTwo" (\a b -> neg (a `dis` b) == (neg a `con` neg b))+ prop "identityOne" (\as b -> conSet as `imp` b == disSet (map neg as) `dis` b)+ 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 "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 ))+ prop "elseOf" (\b -> if b `elem` [bot,top] then elseOf b == b else elseOf b == restrict b (fromJust $ firstVarOf b, False))+ prop "deMorganOneSet" (\as -> neg (conSet as) == disSet (map neg as))+ 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 "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 "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 "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 "relabel" (\b c -> let+ vs = reverse $ nub (allVarsOf b ++ allVarsOf c)+ mapping = zip vs (map (+100) vs)+ 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 1 b c == ifthenelse b (restrict c (1,True)) (restrict c (1,False)))+ prop "show" (\a b -> (show (unravel a) == show (unravel b)) == (a == (b::Bdd)))+ prop "showList" (\a b -> (showList [unravel a] "" == showList [unravel b] "") == (a == (b::Bdd)))+ describe "QuickCheck Expected Failures" $ do+ 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)
− tests/Tautologies.hs
@@ -1,63 +0,0 @@-module Main where--import Control.Monad-import Data.HasCacBDD-import Data.List-import Data.Maybe-import Data.Tuple-import Text.Printf-import Test.QuickCheck-import Test.QuickCheck.Test-import System.Exit--main :: IO ()-main = do- results <- mapM (\(s,a) -> printf "%-25s: " s >> a) tests- unless (all isSuccess results) exitFailure- showInfo--tests :: [(String, IO Result)]-tests =- [("selfEqual", quickCheckResult (\b -> (b::Bdd) == b))- ,("idSymmetry", quickCheckResult (\a b -> ((a::Bdd) == (b::Bdd)) == (b == a)))- ,("singleNegation", quickCheckResult (\b -> neg b /= b))- ,("doubleNegation", quickCheckResult (\b -> neg (neg b) == b))- ,("selfImp", quickCheckResult (\b -> imp b b == top))- ,("selfEqu", quickCheckResult (\b -> equ b b == top))- ,("selfXor", quickCheckResult (\b -> xor b b == bot))- ,("excludedMiddle", quickCheckResult (\b -> b `dis` neg b == top))- ,("deMorganOne", quickCheckResult (\a b -> neg (a `con` b) == (neg a `dis` neg b)))- ,("deMorganTwo", quickCheckResult (\a b -> neg (a `dis` b) == (neg a `con` neg b)))- ,("identityOne", quickCheckResult (\as b -> conSet as `imp` b == disSet (map neg as) `dis` b))- ,("conElim", quickCheckResult (\a b -> imp (con a b) a == top))- ,("conElim3", quickCheckResult (\a b c -> imp (conSet [a, b, c]) a == top))- ,("negNotEqual", quickCheckResult (\b -> neg b /= b))- ,("quantifDuality", quickCheckResult (forAll (elements [0..maximumvar]) (\n b -> forall n b == neg (exists n (neg b)))))- ,("allSats", quickCheckResult (\b -> all (\s -> restrictSet b s == top) (allSats b)))- ,("anySat", quickCheckResult (\b -> if b==bot then isNothing (anySat b) else restrictSet b (fromJust $ anySat b) == top))- ,("ifthenelse", quickCheckResult (\a b c -> ifthenelse a b c == neg (dis (con a (neg b)) (con (neg a) (neg c)))))- ,("ravel-unravel", quickCheckResult (\b -> b == ravel (unravel b)))- ,("firstVarOf", quickCheckResult (\b -> if b `elem` [bot,top] then isNothing (firstVarOf b) else Just (head (allVarsOfSorted b)) == firstVarOf b))- ,("maxVarOf", quickCheckResult (\b -> if b `elem` [bot,top] then isNothing (maxVarOf b) else Just (last (allVarsOfSorted b)) == maxVarOf b))- ,("thenOf", quickCheckResult (\b -> if b `elem` [bot,top] then thenOf b == b else thenOf b == restrict b (fromJust $ firstVarOf b, True )))- ,("elseOf", quickCheckResult (\b -> if b `elem` [bot,top] then elseOf b == b else elseOf b == restrict b (fromJust $ firstVarOf b, False)))- ,("deMorganOneSet", quickCheckResult (\as -> neg (conSet as) == disSet (map neg as)))- ,("deMorganTwoSet", quickCheckResult (\as -> neg (disSet as) == conSet (map neg as)))- ,("xorSetCommute", quickCheckResult (\a as -> xorSet (a:as) == xor (xorSet as) a))- ,("gfpCon", quickCheckResult (\b -> gfp (`con` b) == b))- ,("sizeNeg", quickCheckResult (\b -> sizeOf b == sizeOf (neg b)))- ,("restrictLaw", quickCheckResult (\a b -> b `imp` equ (restrictLaw a b) a == top))- ,("evaluate", quickCheckResult (\b -> all (\s -> evaluate b s == Just True) (allSatsWith (allVarsOf b) b)))- ,("evaluateFun", quickCheckResult (\b -> all (\s -> evaluateFun b (\n -> fromJust $ lookup n s)) (allSats b)))- ,("allSatsWith", quickCheckResult (\b -> all (\s -> restrictSet b s == top) (allSatsWith (allVarsOf b) b)))- ,("anySatWith", quickCheckResult (\b -> let vs = allVarsOf b in if b==bot then isNothing (anySatWith vs b) else restrictSet b (fromJust $ anySatWith vs b) == top))- ,("satCountWith", quickCheckResult (\b -> let vs = allVarsOf b in length (allSatsWith vs b) == satCountWith vs b))- ,("subsOf", quickCheckResult (\b -> all (`elem` subsOf b) (subsOf $ thenOf b)))- , let relabelTest b c = relabel gnippam (relabel mapping b) == b where- vs = reverse $ nub (allVarsOf b ++ allVarsOf c)- mapping = zip vs (map (+100) vs)- gnippam = map swap mapping- in ("relabel", quickCheckResult relabelTest)- , ("show", quickCheckResult (\a b -> (show (unravel a) == show (unravel b)) == (a == (b::Bdd))))- , ("showList", quickCheckResult (\a b -> (showList [unravel a] "" == showList [unravel b] "") == (a == (b::Bdd))))- ]