cudd 0.1.0.0 → 0.1.0.4
raw patch · 5 files changed
Files
- Cudd/C.hs +17/−1
- Cudd/Cudd.hs +17/−0
- Cudd/Imperative.hs +61/−0
- Readme.md +56/−0
- cudd.cabal +57/−16
Cudd/C.hs view
@@ -66,6 +66,8 @@ c_cuddEval, c_cuddCountLeaves, c_cuddCountMinterm,+ c_cuddApaCountMinterm,+ c_cuddFreeApaNumber, c_cuddCountPathsToNonZero, c_cuddCountPath, c_cuddBddConstrain,@@ -95,7 +97,9 @@ c_cuddFirstPrime, c_cuddNextPrime, c_cuddIsGenEmpty,- c_cuddGenFree+ c_cuddGenFree,+ c_cuddFirstNode,+ c_cuddNextNode ) where import Foreign@@ -294,6 +298,12 @@ foreign import ccall safe "Cudd_CountMinterm" c_cuddCountMinterm :: Ptr CDDManager -> Ptr CDDNode -> CInt -> IO CDouble +foreign import ccall safe "Cudd_FreeApaNumber"+ c_cuddFreeApaNumber :: Ptr CInt -> IO () ++foreign import ccall safe "Cudd_ApaCountMinterm"+ c_cuddApaCountMinterm :: Ptr CDDManager -> Ptr CDDNode -> CInt -> Ptr CInt -> IO (Ptr CInt)+ foreign import ccall safe "Cudd_CountPathsToNonZero" c_cuddCountPathsToNonZero :: Ptr CDDNode -> IO CDouble @@ -383,4 +393,10 @@ foreign import ccall safe "Cudd_GenFree" c_cuddGenFree :: Ptr CDDGen -> IO CInt++foreign import ccall safe "Cudd_FirstNode"+ c_cuddFirstNode :: Ptr CDDManager -> Ptr CDDNode -> Ptr (Ptr CDDNode) -> IO (Ptr CDDGen)++foreign import ccall safe "Cudd_NextNode"+ c_cuddNextNode :: Ptr CDDGen -> Ptr (Ptr CDDNode) -> IO CInt
Cudd/Cudd.hs view
@@ -1,5 +1,22 @@ {-# LANGUAGE ForeignFunctionInterface, CPP, FlexibleContexts, RankNTypes #-} +{-| Bindings to the CUDD BDD library++This is a straightforward wrapper around the C library. See <http://vlsi.colorado.edu/~fabio/CUDD/> for documentation.++Exampe usage:++> import Cudd.Cudd+> +> main = do+> let manager = cuddInit+> v1 = ithVar manager 0+> v2 = ithVar manager 1+> conj = bAnd manager v1 v2+> implies = lEq manager conj v1+> print implies+-}+ module Cudd.Cudd ( DDManager(..), DDNode(..),
Cudd/Imperative.hs view
@@ -1,5 +1,25 @@ {-# LANGUAGE RankNTypes #-} +{-| An ST Monad based interface to the CUDD BDD library++This is a straightforward wrapper around the C library. See <http://vlsi.colorado.edu/~fabio/CUDD/> for documentation.++Exampe usage:++> import Control.Monad.ST+> import Cudd.Imperative+> +> main = do+> res <- stToIO $ withManagerDefaults $ \manager -> do+> v1 <- ithVar manager 0+> v2 <- ithVar manager 1+> conj <- bAnd manager v1 v2+> implies <- lEq manager conj v1+> deref manager conj+> return implies+> print res+-}+ module Cudd.Imperative ( DDManager(..), DDNode(..),@@ -73,6 +93,7 @@ quit, readIndex, printMinterm,+ countMintermExact, checkCube, Cube, Prime,@@ -83,6 +104,8 @@ nextCube, firstPrime, nextPrime,+ firstNode,+ nextNode, module Cudd.Common ) where @@ -156,6 +179,7 @@ arg3 :: (Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)) -> DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) arg3 f (DDManager m) (DDNode x) (DDNode y) (DDNode z) = liftM DDNode $ unsafeIOToST $ f m x y z +bZero, bOne :: DDManager s u -> DDNode s u bZero (DDManager m) = DDNode $ unsafePerformIO $ c_cuddReadLogicZero m bOne (DDManager m) = DDNode $ unsafePerformIO $ c_cuddReadOne m @@ -172,7 +196,10 @@ andAbstract = arg3 c_cuddBddAndAbstract xorExistAbstract = arg3 c_cuddBddXorExistAbstract +bNot :: DDNode s u -> DDNode s u bNot (DDNode x) = DDNode $ unsafePerformIO $ c_cuddNotNoRef x++ithVar :: DDManager s u -> Int -> ST s (DDNode s u) ithVar (DDManager m) i = liftM DDNode $ unsafeIOToST $ c_cuddBddIthVar m (fromIntegral i) deref :: DDManager s u -> DDNode s u -> ST s ()@@ -357,11 +384,21 @@ printMinterm :: DDManager s u -> DDNode s u -> ST s () printMinterm (DDManager m) (DDNode x) = unsafeIOToST $ c_cuddPrintMinterm m x +countMintermExact :: DDManager s u -> DDNode s u -> Int -> ST s Integer+countMintermExact (DDManager m) (DDNode x) n = unsafeIOToST $+ alloca $ \ sizep -> do+ apa <- c_cuddApaCountMinterm m x (fromIntegral n) sizep+ size <- fromIntegral <$> peek sizep+ digits <- peekArray size apa+ c_cuddFreeApaNumber apa+ return $ foldl ( \ a d -> a * 2^32 + fromIntegral d ) 0 digits+ checkCube :: DDManager s u -> DDNode s u -> ST s Bool checkCube (DDManager m) (DDNode x) = liftM (==1) $ unsafeIOToST $ c_cuddCheckCube m x data Cube data Prime+data Node data DDGen s u t = DDGen (Ptr CDDGen) genFree :: DDGen s u t -> ST s ()@@ -427,4 +464,28 @@ cubeP <- peek cubePP cube <- peekArray (fromIntegral sz) cubeP return $ Just $ map (toSatBit . fromIntegral) cube++firstNode :: DDManager s u -> DDNode s u -> ST s (Maybe (DDNode s u, DDGen s u Node))+firstNode (DDManager m) (DDNode x) = unsafeIOToST $ do+ alloca $ \nodePP -> do+ gen <- c_cuddFirstNode m x nodePP+ empty <- c_cuddIsGenEmpty gen+ if empty == 1 then do+ c_cuddGenFree gen+ return Nothing+ else do+ nodeP <- peek nodePP+ return $ Just (DDNode nodeP, DDGen gen)++nextNode :: DDManager s u -> DDGen s u Node -> ST s (Maybe (DDNode s u))+nextNode (DDManager m) (DDGen g) = unsafeIOToST $ do+ alloca $ \nodePP -> do+ c_cuddNextNode g nodePP+ empty <- c_cuddIsGenEmpty g+ if empty == 1 then do+ c_cuddGenFree g+ return Nothing+ else do+ nodeP <- peek nodePP+ return $ Just $ DDNode nodeP
+ Readme.md view
@@ -0,0 +1,56 @@+# Haskell-CUDD++Haskell bindings to version 3.0.0 of the CUDD binary decision diagram library.++http://vlsi.colorado.edu/~fabio/CUDD/++This package provides two interfaces to the CUDD library:+* A purely functional one in `Cudd.Cudd` that automatically dereferences BDDs during garbage collection.+* An ST Monad based one in `Cudd.Imperative` that gives you precise control over the ordering of BDD operations and when BDDs are dereferenced. Use this one if you want your code to perform well.++Also, for a higher level interface in the style of the [ersatz](https://hackage.haskell.org/package/ersatz) SAT encoder, see https://github.com/jwaldmann/cudd-ersatz/.++# Installation++Either install CUDD 3.0.0 using your system's package manager or download and install CUDD from here: http://vlsi.colorado.edu/~fabio/.++Then:++`cabal install cudd`++Depending on where CUDD is installed on your system, you may need to provide --extra-lib-dirs or --extra-include-dirs:++`cabal install cudd --extra-lib-dirs=/usr/local/lib`++# Usage++The purely functional interface:++```haskell+import Cudd.Cudd++main = do+ let manager = cuddInit+ v1 = ithVar manager 0+ v2 = ithVar manager 1+ conj = bAnd manager v1 v2+ implies = lEq manager conj v1+ print implies+```++The ST Monad based interface:++```haskell+import Control.Monad.ST+import Cudd.Imperative++main = do+ res <- stToIO $ withManagerDefaults $ \manager -> do+ v1 <- ithVar manager 0+ v2 <- ithVar manager 1+ conj <- bAnd manager v1 v2+ implies <- lEq manager conj v1+ deref manager conj+ return implies+ print res+```
cudd.cabal view
@@ -1,32 +1,73 @@ -- Initial cudd.cabal generated by cabal init. For further -- documentation, see http://haskell.org/cabal/users-guide/ name: cudd-version: 0.1.0.0+version: 0.1.0.4 synopsis: Bindings to the CUDD binary decision diagrams library-description: Bindings to the CUDD binary decision diagrams library. - .- <http://vlsi.colorado.edu/~fabio/CUDD/>+description: + Bindings to version 3.0.0 of the CUDD binary decision diagrams library. + .+ <http://vlsi.colorado.edu/~fabio/CUDD/>+ .+ /Installation/+ .+ Either install CUDD 3.0.0 using your system's package manager or download and install CUDD from here: <http://vlsi.colorado.edu/~fabio/>. + .+ Then:+ .+ "cabal install cudd"+ .+ Depending on where CUDD is installed on your system, you may need to provide --extra-lib-dirs or --extra-include-dirs:+ .+ "cabal install cudd --extra-lib-dirs=\/usr\/local\/lib"+ .+ /Usage/+ .+ This package provides two interfaces to the CUDD library:+ .+ * A purely functional one in "Cudd.Cudd" that automatically dereferences BDDs during garbage collection.+ .+ * An ST Monad based one in "Cudd.Imperative" that gives you precise control over the ordering of BDD operations and when BDDs are dereferenced. Use this one if you want your code to perform well.+ .+ Also, for a higher level interface in the style of the <https://hackage.haskell.org/package/ersatz ersatz> SAT encoder, see <https://github.com/jwaldmann/cudd-ersatz/>.+ license: BSD3 license-file: LICENSE author: Adam Walker maintainer: adamwalker10@gmail.com-copyright: 2014 Adam Walker+copyright: 2016 Adam Walker category: Data homepage: https://github.com/adamwalker/haskell_cudd bug-reports: https://github.com/adamwalker/haskell_cudd/issues build-type: Simple--- extra-source-files: +extra-source-files: Readme.md cabal-version: >=1.10 library- exposed-modules: Cudd.File, Cudd.Convert, Cudd.Reorder, Cudd.MTR, Cudd.Hook, Cudd.Common, Cudd.C, Cudd.Cudd, Cudd.GC, Cudd.Imperative- other-modules: Cudd.ForeignHelpers- other-extensions: ForeignFunctionInterface, CPP, FlexibleContexts, RankNTypes, EmptyDataDecls- build-depends: base >=4.6 && <4.8, mtl >=2.1 && <2.3, array >=0.4 && <0.6, transformers >=0.3 && <0.5- -- hs-source-dirs: - build-tools: c2hs, hsc2hs- default-language: Haskell2010- include-dirs: .- c-sources: c_sources/cuddwrap.c, c_sources/stubs.c- extra-libraries: cudd, mtr, st, util, epd, dddmp, m+ exposed-modules: + Cudd.File, + Cudd.Convert, + Cudd.Reorder, + Cudd.MTR, + Cudd.Hook, + Cudd.Common, + Cudd.C, + Cudd.Cudd, + Cudd.GC, + Cudd.Imperative+ other-modules: Cudd.ForeignHelpers+ other-extensions: ForeignFunctionInterface, CPP, FlexibleContexts, RankNTypes, EmptyDataDecls+ build-depends: + base >=4.7 && <5, + mtl >=2.1 && <2.3, + array >=0.4 && <0.6, + transformers >=0.3 && <0.6+ -- hs-source-dirs: + build-tools: c2hs, hsc2hs+ default-language: Haskell2010+ include-dirs: .+ c-sources: + c_sources/cuddwrap.c, + c_sources/stubs.c+ extra-libraries: cudd, m+