HasCacBDD 0.2.0.0 → 0.3.0.0
raw patch · 8 files changed
+101/−68 lines, 8 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ Data.HasCacBDD: optimalOrder :: Bdd -> [(Int, Int)]
Files
- CHANGELOG.md +6/−0
- HasCacBDD.cabal +3/−3
- README.md +4/−2
- c/BDDNodeC.cpp +21/−21
- c/BDDNodeC.h +23/−21
- hs/Data/HasCacBDD.hs +36/−19
- stack.yaml +1/−1
- tests/Main.hs +7/−1
CHANGELOG.md view
@@ -4,6 +4,12 @@ - ... +## 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) - rename `forall` (soon a keyword in GHC) to `forall_` and `exists` to `exists_`
HasCacBDD.cabal view
@@ -1,5 +1,5 @@ name: HasCacBDD-version: 0.2.0.0+version: 0.3.0.0 synopsis: Haskell bindings for CacBDD homepage: https://github.com/m4lvin/HasCacBDD license: GPL-2@@ -34,8 +34,8 @@ custom-setup setup-depends: base >= 4.8 && < 5,- Cabal < 3.9,- directory+ Cabal < 3.13,+ directory <1.4 library exposed-modules: Data.HasCacBDD,
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. @@ -40,3 +40,5 @@ Var 5 Bot Top λ> dis (neg (var 3)) (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,6 +20,8 @@ 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@@ -31,7 +33,8 @@ import Foreign.Ptr (Ptr) import Foreign (ForeignPtr, newForeignPtr, withForeignPtr, finalizerFree) import System.IO.Unsafe (unsafePerformIO)-import Data.List (nub,(\\),sort)+import Data.Function (on)+import Data.List ((\\), minimumBy, nub, permutations, sort) import Data.Maybe (fromJust) import Test.QuickCheck (Arbitrary, Gen, arbitrary, shrink, choose, oneof, sized, listOf) @@ -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@@ -365,13 +376,13 @@ 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@@ -427,6 +438,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 ()
stack.yaml view
@@ -1,3 +1,3 @@-resolver: lts-21.19+resolver: lts-21.25 packages: - '.'
tests/Main.hs view
@@ -1,7 +1,7 @@ module Main where import Data.HasCacBDD-import Data.List (nub)+import Data.List ((\\),nub) import Data.Maybe (fromJust,isNothing) import Data.Tuple (swap) import Test.QuickCheck@@ -118,11 +118,17 @@ 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 "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 "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" $