diff --git a/Cudd/C.hs b/Cudd/C.hs
--- a/Cudd/C.hs
+++ b/Cudd/C.hs
@@ -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
 
diff --git a/Cudd/Cudd.hs b/Cudd/Cudd.hs
--- a/Cudd/Cudd.hs
+++ b/Cudd/Cudd.hs
@@ -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(..),
diff --git a/Cudd/Imperative.hs b/Cudd/Imperative.hs
--- a/Cudd/Imperative.hs
+++ b/Cudd/Imperative.hs
@@ -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
 
diff --git a/Readme.md b/Readme.md
new file mode 100644
--- /dev/null
+++ b/Readme.md
@@ -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
+```
diff --git a/cudd.cabal b/cudd.cabal
--- a/cudd.cabal
+++ b/cudd.cabal
@@ -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
+