diff --git a/Cudd/C.hs b/Cudd/C.hs
new file mode 100644
--- /dev/null
+++ b/Cudd/C.hs
@@ -0,0 +1,386 @@
+{-# LANGUAGE ForeignFunctionInterface, EmptyDataDecls, CPP #-}
+
+module Cudd.C (
+    CDDManager,
+    CDDNode,
+    CDDGen,
+    c_cuddReadOne,
+    c_cuddReadLogicZero,
+    c_cuddReadOneWithRef,
+    c_cuddReadLogicZeroWithRef,
+    c_cuddBddIthVar,
+    c_cuddBddAnd,
+    c_cuddBddOr,
+    c_cuddBddNand,
+    c_cuddBddNor,
+    c_cuddBddXor,
+    c_cuddBddXnor,
+    c_cuddNot,
+    c_cuddNotNoRef,
+    c_cuddBddIte,
+    c_cuddBddExistAbstract,
+    c_cuddBddUnivAbstract,
+    c_cuddIterDerefBdd,
+    cuddRef,
+    c_cuddInit,
+    c_cuddShuffleHeap,
+    c_cuddSetVarMap,
+    c_cuddBddVarMap,
+    c_cuddBddLeq,
+    c_cuddBddSwapVariables,
+    c_cuddLargestCube,
+    c_cuddBddMakePrime,
+    c_cuddSupport,
+    c_cuddSupportIndex,
+    c_cuddSupportIndices,
+    c_cuddIndicesToCube,
+    c_cuddBddComputeCube,
+    c_cuddBddToCubeArray,
+    c_cuddReadSize,
+    c_cuddBddCompose,
+    c_cuddBddAndAbstract,
+    c_cuddBddXorExistAbstract,
+    c_cuddBddLeqUnless,
+    c_cuddEquivDC,
+    c_cuddXeqy,
+    c_cuddDebugCheck,
+    c_cuddCheckKeys,
+    c_cuddBddPickOneMinterm,
+    c_cuddCheckZeroRef,
+    c_cuddReadInvPerm,
+    c_cuddReadPerm,
+    c_cuddDagSize,
+    c_cuddReadNodeCount,
+    c_cuddReadPeakNodeCount,
+    c_cuddReadMaxCache,
+    c_cuddReadMaxCacheHard,
+    c_cuddSetMaxCacheHard,
+    c_cuddReadCacheSlots,
+    c_cuddReadCacheUsedSlots,
+    c_cuddBddAndLimit,
+    c_cuddBddNewVarAtLevel,
+    c_cuddReadTree,
+    c_cuddBddLICompaction,
+    c_cuddBddSqueeze,
+    c_cuddBddMinimize,
+    c_cuddEval,
+    c_cuddCountLeaves,
+    c_cuddCountMinterm,
+    c_cuddCountPathsToNonZero,
+    c_cuddCountPath,
+    c_cuddBddConstrain,
+    c_cuddBddRestrict,
+    c_wrappedRegular,
+    c_cuddBddPermute,
+    c_cuddXgty,
+    c_cuddInequality,
+    c_cuddDisequality,
+    c_cuddBddInterval,
+    c_cuddNodeReadIndex,
+    c_cuddBddTransfer,
+    c_cuddRecursiveDerefPtr,
+    c_cuddDelayedDerefBddPtr,
+    c_cuddIterDerefBddPtr,
+    c_cuddBddNewVar,
+    c_cuddBddVectorCompose,
+    c_cuddQuit,
+    c_cuddPrintMinterm,
+    c_cuddCheckCube,
+    c_cuddPrintInfo,
+    c_cuddPrintDebug,
+    c_cuddIsComplement,
+    c_cuddDumpDot,
+    c_cuddFirstCube,
+    c_cuddNextCube,
+    c_cuddFirstPrime,
+    c_cuddNextPrime,
+    c_cuddIsGenEmpty,
+    c_cuddGenFree
+    ) where
+
+import Foreign
+import Foreign.C.Types
+import Foreign.C.String
+
+import Cudd.MTR
+
+data CDDManager
+data CDDNode
+data CDDGen
+
+foreign import ccall safe "Cudd_ReadOne_s"
+	c_cuddReadOne :: Ptr CDDManager -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_ReadLogicZero_s"
+	c_cuddReadLogicZero :: Ptr CDDManager -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_ReadOne_withRef_s"
+	c_cuddReadOneWithRef :: Ptr CDDManager -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_ReadLogicZero_withRef_s"
+	c_cuddReadLogicZeroWithRef :: Ptr CDDManager -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddIthVar_s"
+	c_cuddBddIthVar :: Ptr CDDManager -> CInt -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddAnd_s"
+	c_cuddBddAnd :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddOr_s"
+	c_cuddBddOr :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddNand_s"
+	c_cuddBddNand :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddNor_s"
+	c_cuddBddNor :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddXor_s"
+	c_cuddBddXor :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddXnor_s"
+	c_cuddBddXnor :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_Not_s"
+	c_cuddNot :: Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_NotNoRef_s"
+	c_cuddNotNoRef :: Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddIte_s"
+    c_cuddBddIte :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddExistAbstract_s"
+	c_cuddBddExistAbstract :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddUnivAbstract_s"
+	c_cuddBddUnivAbstract :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_IterDerefBdd"
+	c_cuddIterDerefBdd :: Ptr CDDManager -> Ptr CDDNode -> IO ()
+
+foreign import ccall safe "wrappedCuddRef"
+	cuddRef :: Ptr CDDNode -> IO ()
+
+foreign import ccall safe "Cudd_Init"
+	c_cuddInit :: CInt -> CInt -> CInt -> CInt -> CInt -> IO (Ptr CDDManager)
+
+foreign import ccall safe "Cudd_ShuffleHeap"
+    c_cuddShuffleHeap :: Ptr CDDManager -> Ptr CInt -> IO CInt
+
+foreign import ccall safe "Cudd_SetVarMap"
+    c_cuddSetVarMap :: Ptr CDDManager -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> CInt -> IO CInt
+
+foreign import ccall safe "Cudd_bddVarMap_s"
+    c_cuddBddVarMap :: Ptr CDDManager -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddLeq"
+    c_cuddBddLeq :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO CInt
+
+foreign import ccall safe "Cudd_bddSwapVariables_s"
+    c_cuddBddSwapVariables :: Ptr CDDManager -> Ptr CDDNode -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> CInt -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_LargestCube_s"
+    c_cuddLargestCube :: Ptr CDDManager -> Ptr CDDNode -> Ptr CInt -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddMakePrime_s"
+    c_cuddBddMakePrime :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_Support_s"
+    c_cuddSupport :: Ptr CDDManager -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_SupportIndex"
+	c_cuddSupportIndex :: Ptr CDDManager -> Ptr CDDNode -> IO(Ptr CInt)
+
+foreign import ccall safe "Cudd_SupportIndices"
+    c_cuddSupportIndices :: Ptr CDDManager -> Ptr CDDNode -> Ptr (Ptr CInt) -> IO CInt
+
+foreign import ccall safe "Cudd_IndicesToCube_s"
+    c_cuddIndicesToCube :: Ptr CDDManager -> Ptr CInt -> CInt -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddComputeCube_s"
+    c_cuddBddComputeCube :: Ptr CDDManager -> Ptr (Ptr CDDNode) -> Ptr CInt -> CInt -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_BddToCubeArray"
+    c_cuddBddToCubeArray :: Ptr CDDManager -> Ptr CDDNode -> Ptr CInt -> IO CInt
+
+foreign import ccall safe "Cudd_ReadSize"
+	c_cuddReadSize :: Ptr CDDManager -> IO CInt
+
+foreign import ccall safe "Cudd_bddCompose_s"
+    c_cuddBddCompose :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> CInt -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddAndAbstract_s"
+    c_cuddBddAndAbstract :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddXorExistAbstract_s"
+    c_cuddBddXorExistAbstract :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddLeqUnless"
+    c_cuddBddLeqUnless :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO CInt
+
+foreign import ccall safe "Cudd_EquivDC"
+    c_cuddEquivDC :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO CInt
+
+foreign import ccall safe "Cudd_Xeqy_s"
+	c_cuddXeqy :: Ptr CDDManager -> CInt -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_DebugCheck"
+    c_cuddDebugCheck :: Ptr CDDManager -> IO CInt
+
+foreign import ccall safe "Cudd_CheckKeys"
+    c_cuddCheckKeys :: Ptr CDDManager -> IO CInt
+
+foreign import ccall safe "Cudd_bddPickOneMinterm_s"
+	c_cuddBddPickOneMinterm :: Ptr CDDManager -> Ptr CDDNode -> Ptr (Ptr CDDNode) -> CInt -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_CheckZeroRef"
+    c_cuddCheckZeroRef :: Ptr CDDManager -> IO CInt
+
+foreign import ccall safe "Cudd_ReadInvPerm"
+    c_cuddReadInvPerm :: Ptr CDDManager -> CInt -> IO CInt
+
+foreign import ccall safe "Cudd_ReadPerm"
+    c_cuddReadPerm :: Ptr CDDManager -> CInt -> IO CInt
+
+foreign import ccall safe "Cudd_DagSize"
+    c_cuddDagSize :: Ptr CDDNode -> IO CInt
+
+foreign import ccall safe "Cudd_ReadNodeCount"
+    c_cuddReadNodeCount :: Ptr CDDManager -> IO CLong
+
+foreign import ccall safe "Cudd_ReadPeakNodeCount"
+    c_cuddReadPeakNodeCount :: Ptr CDDManager -> IO CLong
+
+foreign import ccall safe "Cudd_ReadMaxCache"
+    c_cuddReadMaxCache :: Ptr CDDManager -> IO CInt
+
+foreign import ccall safe "Cudd_ReadMaxCacheHard"
+    c_cuddReadMaxCacheHard :: Ptr CDDManager -> IO CInt
+
+foreign import ccall safe "Cudd_SetMaxCacheHard"
+    c_cuddSetMaxCacheHard :: Ptr CDDManager -> CInt -> IO ()
+
+foreign import ccall safe "Cudd_ReadCacheSlots"
+    c_cuddReadCacheSlots :: Ptr CDDManager -> IO CInt
+
+foreign import ccall safe "Cudd_ReadCacheUsedSlots"
+    c_cuddReadCacheUsedSlots :: Ptr CDDManager -> IO CInt
+
+foreign import ccall safe "Cudd_bddAndLimit"
+    c_cuddBddAndLimit :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> CUInt -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddNewVarAtLevel_s"
+    c_cuddBddNewVarAtLevel :: Ptr CDDManager -> CInt -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_ReadTree"
+    c_cuddReadTree :: Ptr CDDManager -> IO (Ptr CMtrNode)
+
+foreign import ccall safe "Cudd_bddLICompaction_s"
+    c_cuddBddLICompaction :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddSqueeze_s" 
+    c_cuddBddSqueeze :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddMinimize_s"
+    c_cuddBddMinimize :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_Eval"
+    c_cuddEval :: Ptr CDDManager -> Ptr CDDNode -> Ptr CInt -> IO (Ptr CDDNode)
+
+foreign import ccall safe ",h Cudd_CountLeaves"
+    c_cuddCountLeaves :: Ptr CDDNode -> IO CInt
+
+foreign import ccall safe "Cudd_CountMinterm"
+    c_cuddCountMinterm :: Ptr CDDManager -> Ptr CDDNode -> CInt -> IO CDouble
+
+foreign import ccall safe "Cudd_CountPathsToNonZero"
+    c_cuddCountPathsToNonZero :: Ptr CDDNode -> IO CDouble
+
+foreign import ccall safe "Cudd_CountPath"
+    c_cuddCountPath :: Ptr CDDNode -> IO CDouble
+
+foreign import ccall safe "Cudd_bddConstrain_s"
+    c_cuddBddConstrain :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddRestrict_s"
+    c_cuddBddRestrict :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "wrappedRegular"
+    c_wrappedRegular :: Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddPermute_s"
+    c_cuddBddPermute :: Ptr CDDManager -> Ptr CDDNode -> Ptr CInt -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_Xgty_s"
+	c_cuddXgty :: Ptr CDDManager -> CInt -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_Inequality_s"
+	c_cuddInequality :: Ptr CDDManager -> CInt -> CInt -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_Disequality_s"
+	c_cuddDisequality :: Ptr CDDManager -> CInt -> CInt -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddInterval_s"
+    c_cuddBddInterval :: Ptr CDDManager -> CInt -> Ptr (Ptr CDDNode) -> CInt -> CInt -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_NodeReadIndex"
+    c_cuddNodeReadIndex :: Ptr CDDNode -> IO CInt
+
+foreign import ccall safe "Cudd_bddTransfer"
+    c_cuddBddTransfer :: Ptr CDDManager -> Ptr CDDManager -> Ptr CDDNode -> IO (Ptr CDDNode)
+
+foreign import ccall safe "&Cudd_RecursiveDeref"
+	c_cuddRecursiveDerefPtr :: FunPtr (Ptr CDDManager -> Ptr CDDNode -> IO ())
+
+foreign import ccall safe "&Cudd_DelayedDerefBdd"
+	c_cuddDelayedDerefBddPtr :: FunPtr (Ptr CDDManager -> Ptr CDDNode -> IO ())
+
+foreign import ccall safe "&Cudd_IterDerefBdd"
+	c_cuddIterDerefBddPtr :: FunPtr (Ptr CDDManager -> Ptr CDDNode -> IO ())
+
+foreign import ccall safe "Cudd_bddNewVar_s"
+    c_cuddBddNewVar :: Ptr CDDManager -> IO (Ptr CDDNode)
+
+foreign import ccall safe "Cudd_bddVectorCompose_s"
+    c_cuddBddVectorCompose :: Ptr CDDManager -> Ptr CDDNode -> Ptr (Ptr CDDNode) -> IO (Ptr CDDNode) 
+
+foreign import ccall safe "Cudd_Quit"
+    c_cuddQuit :: Ptr CDDManager -> IO ()
+
+foreign import ccall safe "Cudd_PrintMinterm"
+    c_cuddPrintMinterm :: Ptr CDDManager -> Ptr CDDNode -> IO ()
+
+foreign import ccall safe "Cudd_CheckCube"
+    c_cuddCheckCube :: Ptr CDDManager -> Ptr CDDNode -> IO CInt
+
+foreign import ccall safe "Cudd_PrintInfo"
+       c_cuddPrintInfo :: Ptr CDDManager -> Ptr CFile -> IO CInt
+
+foreign import ccall safe "Cudd_PrintDebug"
+    c_cuddPrintDebug :: Ptr CDDManager -> Ptr CDDNode -> CInt -> CInt -> IO CInt
+
+foreign import ccall safe "wrappedCuddIsComplement"
+    c_cuddIsComplement :: Ptr CDDNode -> CInt
+
+foreign import ccall safe "Cudd_DumpDot"
+    c_cuddDumpDot :: Ptr CDDManager -> CInt -> Ptr (Ptr CDDNode) -> Ptr CString -> Ptr CString -> Ptr CFile -> IO CInt
+
+foreign import ccall safe "Cudd_FirstCube"
+    c_cuddFirstCube :: Ptr CDDManager -> Ptr CDDNode -> Ptr (Ptr CInt) -> Ptr CInt -> IO (Ptr CDDGen)
+
+foreign import ccall safe "Cudd_NextCube"
+    c_cuddNextCube :: Ptr CDDGen -> Ptr (Ptr CInt) -> Ptr CInt -> IO CInt
+
+foreign import ccall safe "Cudd_FirstPrime"
+    c_cuddFirstPrime :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr (Ptr CInt) -> IO (Ptr CDDGen)
+
+foreign import ccall safe "Cudd_NextPrime"
+    c_cuddNextPrime :: Ptr CDDGen -> Ptr (Ptr CInt) -> IO CInt
+
+foreign import ccall safe "Cudd_IsGenEmpty"
+    c_cuddIsGenEmpty :: Ptr CDDGen -> IO CInt
+
+foreign import ccall safe "Cudd_GenFree"
+    c_cuddGenFree :: Ptr CDDGen -> IO CInt
+
diff --git a/Cudd/Common.hsc b/Cudd/Common.hsc
new file mode 100644
--- /dev/null
+++ b/Cudd/Common.hsc
@@ -0,0 +1,30 @@
+module Cudd.Common (
+    SatBit(..),
+    toSatBit,
+    expand,
+    cudd_unique_slots,
+    cudd_cache_slots
+    ) where
+
+#include <stdio.h>
+#include "cudd.h"
+
+data SatBit = Zero | One | DontCare deriving (Eq)
+
+toSatBit :: Int -> SatBit
+toSatBit 0 = Zero
+toSatBit 1 = One
+toSatBit 2 = DontCare
+toSatBit _ = error "toSatBit: Invalid sat bit returned from CUDD"
+
+expand :: SatBit -> [Bool]
+expand Zero     = [False]
+expand One      = [True]
+expand DontCare = [False, True]
+
+cudd_unique_slots :: Int
+cudd_unique_slots = #const CUDD_UNIQUE_SLOTS
+
+cudd_cache_slots :: Int
+cudd_cache_slots = #const CUDD_CACHE_SLOTS
+
diff --git a/Cudd/Convert.hs b/Cudd/Convert.hs
new file mode 100644
--- /dev/null
+++ b/Cudd/Convert.hs
@@ -0,0 +1,33 @@
+module Cudd.Convert (
+    fromImperativeNode,
+    fromImperativeManager,
+    toImperativeNode,
+    toImperativeManager
+    ) where
+
+import System.IO.Unsafe
+import Foreign.ForeignPtr
+import Foreign.ForeignPtr.Unsafe
+import Control.Monad.ST
+import Control.Monad.ST.Unsafe
+
+import Cudd.Cudd as C
+import Cudd.C
+import Cudd.Imperative as I hiding (deref)
+
+fromImperativeNode :: C.DDManager -> I.DDNode s u -> C.DDNode
+fromImperativeNode (C.DDManager m) (I.DDNode d) = C.DDNode $ unsafePerformIO $ do 
+    cuddRef d
+    newForeignPtrEnv deref m d
+
+fromImperativeManager :: I.DDManager s u -> C.DDManager
+fromImperativeManager = C.DDManager . I.unDDManager
+
+toImperativeNode :: C.DDNode -> ST s (I.DDNode s u)
+toImperativeNode (C.DDNode fp) = unsafeIOToST $ do
+    let p = unsafeForeignPtrToPtr fp
+    cuddRef p
+    return $ I.DDNode p
+
+toImperativeManager :: C.DDManager -> I.DDManager s u
+toImperativeManager (C.DDManager m) = I.DDManager m
diff --git a/Cudd/Cudd.hs b/Cudd/Cudd.hs
new file mode 100644
--- /dev/null
+++ b/Cudd/Cudd.hs
@@ -0,0 +1,418 @@
+{-# LANGUAGE ForeignFunctionInterface, CPP, FlexibleContexts, RankNTypes #-}
+
+module Cudd.Cudd (
+    DDManager(..),
+    DDNode(..),
+    deref,
+    cuddInit,
+    cuddInitOrder,
+    readOne,
+    readLogicZero,
+    ithVar,
+    bAnd,
+    bOr,
+    bNand,
+    bNor,
+    bXor,
+    bXnor,
+    bNot,
+    dumpDot',
+    dumpDot,
+    cudd_cache_slots,
+    cudd_unique_slots,
+    eval,
+    printMinterm,
+    allSat,
+    oneSat,
+    onePrime,
+    supportIndex,
+    bExists,
+    bForall,
+    bIte,
+    permute,
+    swapVariables,
+    nodeReadIndex,
+    dagSize,
+    indicesToCube,
+    liCompaction,
+    minimize,
+    readSize,
+    xEqY,
+    xGtY,
+    interval,
+    disequality,
+    inequality,
+    ddNodeToInt,
+    pickOneMinterm,
+    readPerm,
+    readInvPerm,
+    readPerms,
+    readInvPerms,
+    readTree,
+    countLeaves,
+    countMinterm,
+    countPath,
+    countPathsToNonZero,
+    printDebug,
+    andAbstract,
+    xorExistAbstract,
+    transfer,
+    makePrime,
+    constrain,
+    restrict,
+    squeeze,
+    SatBit(..),
+    largestCube,
+    lEq,
+    printInfo
+    ) where
+
+import Foreign.Storable
+import Foreign.Ptr
+import Foreign.C.Types
+import Foreign.C.String
+import Foreign.ForeignPtr
+import Foreign.ForeignPtr.Unsafe
+import Foreign.Marshal.Alloc
+import Foreign.Marshal.Array
+import Foreign.Marshal.Utils
+import System.IO.Unsafe
+import Control.Monad
+import Data.List
+
+import Cudd.ForeignHelpers
+import Cudd.MTR
+import Cudd.C
+import Cudd.Common
+
+newtype DDManager = DDManager (Ptr CDDManager)
+newtype DDNode    = DDNode    {unDDNode :: ForeignPtr CDDNode} deriving (Ord, Eq, Show)
+
+deref = c_cuddIterDerefBddPtr
+
+cuddInit :: DDManager
+cuddInit = DDManager $ unsafePerformIO $ c_cuddInit 0 0 (fromIntegral cudd_unique_slots) (fromIntegral cudd_cache_slots) 0
+
+cuddInitOrder :: [Int] -> DDManager
+cuddInitOrder order = DDManager $ unsafePerformIO $ withArrayLen (map fromIntegral order) $ \size ptr -> do
+    when (sort order /= [0..size-1]) (error "cuddInitOrder: order does not contain each variable once") 
+    m <- c_cuddInit (fromIntegral size) 0 (fromIntegral cudd_unique_slots) (fromIntegral cudd_cache_slots) 0
+    res <- c_cuddShuffleHeap m ptr
+    when (res /= 1) (error "shuffleHeap failed")
+    return m
+
+cuddArg0 :: (Ptr CDDManager -> IO (Ptr CDDNode)) -> DDManager -> DDNode
+cuddArg0 f (DDManager m) = DDNode $ unsafePerformIO $ do
+    node <- f m 
+    newForeignPtrEnv deref m node
+
+cuddArg1 :: (Ptr CDDManager -> Ptr CDDNode -> IO (Ptr CDDNode)) -> DDManager -> DDNode -> DDNode
+cuddArg1 f (DDManager m) (DDNode x) = DDNode $ unsafePerformIO $ 
+	withForeignPtr x $ \xp -> do
+	node <- f m xp
+	newForeignPtrEnv deref m node
+
+cuddArg2 :: (Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)) -> DDManager -> DDNode -> DDNode -> DDNode
+cuddArg2 f (DDManager m) (DDNode l) (DDNode r) = DDNode $ unsafePerformIO $ 
+ 	withForeignPtr l $ \lp -> 
+	withForeignPtr r $ \rp -> do
+	node <- f m lp rp
+	newForeignPtrEnv deref m node
+
+cuddArg3 :: (Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)) -> DDManager -> DDNode -> DDNode-> DDNode -> DDNode
+cuddArg3 f (DDManager m) (DDNode l) (DDNode r) (DDNode x) = DDNode $ unsafePerformIO $ 
+ 	withForeignPtr l $ \lp -> 
+	withForeignPtr r $ \rp -> 
+	withForeignPtr x $ \xp -> do
+	node <- f m lp rp xp
+	newForeignPtrEnv deref m node
+
+readOne :: DDManager -> DDNode
+readOne = cuddArg0 c_cuddReadOneWithRef
+
+readLogicZero :: DDManager -> DDNode
+readLogicZero  = cuddArg0 c_cuddReadLogicZeroWithRef
+
+ithVar :: DDManager -> Int -> DDNode
+ithVar m i = cuddArg0 (flip c_cuddBddIthVar (fromIntegral i)) m
+
+bAnd :: DDManager -> DDNode -> DDNode -> DDNode
+bAnd = cuddArg2 c_cuddBddAnd
+
+bOr :: DDManager -> DDNode -> DDNode -> DDNode
+bOr = cuddArg2 c_cuddBddOr
+
+bNand :: DDManager -> DDNode -> DDNode -> DDNode
+bNand = cuddArg2 c_cuddBddNand
+
+bNor :: DDManager -> DDNode -> DDNode -> DDNode
+bNor = cuddArg2 c_cuddBddNor
+
+bXor :: DDManager -> DDNode -> DDNode -> DDNode
+bXor = cuddArg2 c_cuddBddXor
+
+bXnor :: DDManager -> DDNode -> DDNode -> DDNode
+bXnor = cuddArg2 c_cuddBddXnor
+
+bNot :: DDManager -> DDNode -> DDNode
+bNot = cuddArg1 (const c_cuddNot)
+
+dumpDot' :: DDManager -> [DDNode] -> Maybe [String] -> Maybe [String] -> Ptr CFile -> IO Int
+dumpDot' (DDManager m) nodes iNames oNames file = liftM fromIntegral $
+    withForeignArrayPtrLen (map unDDNode nodes) $ \nn np -> 
+        maybe ($ nullPtr) withStringArrayPtr iNames $ \iNamesP -> 
+            maybe ($ nullPtr) withStringArrayPtr oNames $ \oNamesP -> do
+                c_cuddDumpDot m (fromIntegral nn) np iNamesP oNamesP file
+
+foreign import ccall safe "fopen" 
+    c_fopen :: CString -> CString -> IO (Ptr CFile)
+
+foreign import ccall safe "fclose"
+    c_fclose :: (Ptr CFile) -> IO ()
+
+dumpDot :: DDManager -> DDNode -> String -> IO Int
+dumpDot m n fName = 
+    withCAString fName $ \fNameP -> 
+        withCAString "w" $ \md -> do
+            file <- c_fopen fNameP md
+            res <- dumpDot' m [n] Nothing Nothing file
+            c_fclose file
+            return res
+
+eval :: DDManager -> DDNode -> [Int] -> Bool
+eval (DDManager m) (DDNode n) a = unsafePerformIO $ do
+    res <- withArray (map fromIntegral a) $ \ap -> 
+        withForeignPtr n $ \np -> 
+            c_cuddEval m np ap
+    return $ (==0) $ c_cuddIsComplement res
+
+printMinterm :: DDManager -> DDNode -> IO ()
+printMinterm (DDManager m) (DDNode n) = 
+    withForeignPtr n $ c_cuddPrintMinterm m 
+
+foreign import ccall safe "allSat"
+    c_allSat :: Ptr CDDManager -> Ptr CDDNode -> Ptr CInt -> Ptr CInt -> IO (Ptr (Ptr CInt))
+
+foreign import ccall safe "oneSat"
+    c_oneSat :: Ptr CDDManager -> Ptr CDDNode -> Ptr CInt -> IO (Ptr CInt)
+
+allSat :: DDManager -> DDNode -> [[SatBit]]
+allSat (DDManager m) (DDNode n) = unsafePerformIO $ 
+    alloca $ \nvarsptr -> 
+    alloca $ \ntermsptr -> 
+    withForeignPtr n $ \np -> do
+    res <- c_allSat m np ntermsptr nvarsptr
+    nterms <- liftM fromIntegral $ peek ntermsptr
+    res <- peekArray nterms res
+    nvars <- liftM fromIntegral $ peek nvarsptr
+    res <- mapM (peekArray nvars) res
+    return $ map (map (toSatBit . fromIntegral)) res
+
+oneSat :: DDManager -> DDNode -> Maybe [SatBit]
+oneSat (DDManager m) (DDNode n) = unsafePerformIO $ 
+    alloca $ \nvarsptr ->
+    withForeignPtr n $ \np -> do
+    res <- c_oneSat m np nvarsptr
+    if res==nullPtr then return Nothing else do
+        nvars <- liftM fromIntegral $ peek nvarsptr
+        res <- peekArray nvars res
+        return $ Just $ map (toSatBit . fromIntegral) res
+
+foreign import ccall safe "onePrime"
+    c_onePrime :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CInt -> IO (Ptr CInt)
+
+onePrime :: DDManager -> DDNode -> DDNode -> Maybe [Int]
+onePrime (DDManager m) (DDNode l) (DDNode u) = unsafePerformIO $ 
+    alloca $ \nvarsptr -> 
+    withForeignPtr l $ \lp -> 
+    withForeignPtr u $ \up -> do
+    res <- c_onePrime m lp up nvarsptr 
+    if res==nullPtr then return Nothing else do
+        nvars <- liftM fromIntegral $ peek nvarsptr
+        res <- peekArray nvars res
+        return $ Just $ map fromIntegral res
+
+readSize :: DDManager -> Int
+readSize (DDManager m) = fromIntegral $ unsafePerformIO $ c_cuddReadSize m
+
+supportIndex :: DDManager -> DDNode -> [Bool]
+supportIndex (DDManager m) (DDNode n) = unsafePerformIO $ 
+	withForeignPtr n $ \np -> do
+    res <- c_cuddSupportIndex m np
+    size <- c_cuddReadSize m
+    res <- peekArray (fromIntegral size) res
+    return $ map toBool res
+
+bExists :: DDManager -> DDNode -> DDNode -> DDNode
+bExists = cuddArg2 c_cuddBddExistAbstract
+
+bForall :: DDManager -> DDNode -> DDNode -> DDNode
+bForall = cuddArg2 c_cuddBddUnivAbstract
+
+bIte :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode
+bIte = cuddArg3 c_cuddBddIte
+
+swapVariables :: DDManager -> DDNode -> [DDNode] -> [DDNode] -> DDNode
+swapVariables (DDManager m) (DDNode d) s1 s2 = DDNode $ unsafePerformIO $ 
+    withForeignPtr d $ \dp -> 
+    withForeignArrayPtrLen (map unDDNode s1) $ \s1 s1ps -> 
+    withForeignArrayPtrLen (map unDDNode s2) $ \s2 s2ps -> do
+    when (s1 /= s2) (error "cuddBddSwapVariables: variable lists have different sizes")
+    node <- c_cuddBddSwapVariables m dp s1ps s2ps (fromIntegral s1)
+    newForeignPtrEnv deref m node
+
+permute :: DDManager -> DDNode -> [Int] -> DDNode 
+permute (DDManager m) (DDNode d) indexes = DDNode $ unsafePerformIO $ 
+    withForeignPtr d $ \dp -> 
+    withArray (map fromIntegral indexes) $ \ip -> do
+    node <- c_cuddBddPermute m dp ip 
+    newForeignPtrEnv deref m node
+
+xGtY :: DDManager -> [DDNode] -> [DDNode] -> DDNode
+xGtY (DDManager m) x y = DDNode $ unsafePerformIO $ 
+    withForeignArrayPtrLen (map unDDNode x) $ \xl xp -> 
+    withForeignArrayPtrLen (map unDDNode y) $ \yl yp -> do
+    when (xl /= yl) (error "cuddXgty: variable lists have different sizes")
+    node <- c_cuddXgty m (fromIntegral xl) nullPtr xp yp
+    newForeignPtrEnv deref m node
+
+xEqY :: DDManager -> [DDNode] -> [DDNode] -> DDNode
+xEqY (DDManager m) x y = DDNode $ unsafePerformIO $ 
+    withForeignArrayPtrLen (map unDDNode x) $ \xl xp -> 
+    withForeignArrayPtrLen (map unDDNode y) $ \yl yp -> do
+    when (xl /= yl) (error "cuddXeqy: variable lists have different sizes")
+    node <- c_cuddXeqy m (fromIntegral xl) xp yp
+    newForeignPtrEnv deref m node
+
+inequality :: DDManager -> Int -> Int -> [DDNode] -> [DDNode] -> DDNode
+inequality (DDManager m) n c x y = DDNode $ unsafePerformIO $ 
+    withForeignArrayPtr (map unDDNode x) $ \xp -> 
+    withForeignArrayPtr (map unDDNode y) $ \yp -> do
+    node <- c_cuddInequality m (fromIntegral n) (fromIntegral c) xp yp
+    newForeignPtrEnv deref m node
+
+disequality :: DDManager -> Int -> Int -> [DDNode] -> [DDNode] -> DDNode
+disequality (DDManager m) n c x y = DDNode $ unsafePerformIO $
+    withForeignArrayPtr (map unDDNode x) $ \xp -> 
+    withForeignArrayPtr (map unDDNode y) $ \yp -> do
+    node <- c_cuddDisequality m (fromIntegral n) (fromIntegral c) xp yp
+    newForeignPtrEnv deref m node
+
+interval :: DDManager -> [DDNode] -> Int -> Int -> DDNode
+interval (DDManager m) vararr lower upper =  DDNode $ unsafePerformIO $ 
+    withForeignArrayPtrLen (map unDDNode vararr) $ \sz vp -> do
+    node <- c_cuddBddInterval m (fromIntegral sz) vp (fromIntegral lower) (fromIntegral upper)
+    newForeignPtrEnv deref m node
+
+nodeReadIndex :: DDNode -> Int
+nodeReadIndex (DDNode d) = fromIntegral $ unsafePerformIO $ withForeignPtr d c_cuddNodeReadIndex 
+
+dagSize :: DDNode -> Int
+dagSize (DDNode d) = fromIntegral $ unsafePerformIO $ withForeignPtr d c_cuddDagSize 
+
+indicesToCube :: DDManager -> [Int] -> DDNode
+indicesToCube (DDManager m) indices = DDNode $ unsafePerformIO $ 
+    withArrayLen (map fromIntegral indices) $ \size ip -> do
+    node <- c_cuddIndicesToCube m ip (fromIntegral size)
+    newForeignPtrEnv deref m node
+
+liCompaction :: DDManager -> DDNode -> DDNode -> DDNode
+liCompaction = cuddArg2 c_cuddBddLICompaction
+
+minimize :: DDManager -> DDNode -> DDNode -> DDNode
+minimize = cuddArg2 c_cuddBddMinimize
+
+pickOneMinterm :: DDManager -> DDNode -> [DDNode] -> Maybe DDNode
+pickOneMinterm (DDManager m) (DDNode d) vars = unsafePerformIO $
+	withForeignPtr d $ \dp -> 
+	withForeignArrayPtrLen (map unDDNode vars) $ \vs vp -> do
+	node <- c_cuddBddPickOneMinterm m dp vp (fromIntegral vs)
+	if node == nullPtr then return Nothing else do
+		nd <- newForeignPtrEnv deref m node
+		return $ Just $ DDNode nd
+
+printInfo :: DDManager -> Ptr CFile -> IO Int
+printInfo (DDManager m) cf = liftM fromIntegral $ c_cuddPrintInfo m cf
+
+readPerm :: DDManager -> Int -> Int
+readPerm (DDManager m) i = fromIntegral $ unsafePerformIO $ c_cuddReadPerm m (fromIntegral i)
+
+readInvPerm :: DDManager -> Int -> Int
+readInvPerm (DDManager m) i = fromIntegral $ unsafePerformIO $ c_cuddReadInvPerm m (fromIntegral i)
+
+readPerms :: DDManager -> [Int]
+readPerms m = map (readPerm m) [0..(readSize m - 1)]
+
+readInvPerms :: DDManager -> [Int]
+readInvPerms m = map (readInvPerm m) [0..(readSize m -1)]
+
+readTree :: DDManager -> IO (Ptr CMtrNode) 
+readTree (DDManager m) = c_cuddReadTree m
+
+countLeaves :: DDNode -> Int
+countLeaves (DDNode d) = fromIntegral $ unsafePerformIO $ 
+    withForeignPtr d $ \dp -> 
+    c_cuddCountLeaves dp
+
+countMinterm :: DDManager -> DDNode -> Int -> Double
+countMinterm (DDManager m) (DDNode d) n = realToFrac $ unsafePerformIO $
+    withForeignPtr d $ \dp -> 
+    c_cuddCountMinterm m dp (fromIntegral n) 
+
+countPathsToNonZero :: DDNode -> Double
+countPathsToNonZero (DDNode d) = realToFrac $ unsafePerformIO $
+    withForeignPtr d $ \dp ->
+    c_cuddCountPathsToNonZero dp
+
+countPath :: DDNode -> Double
+countPath (DDNode d) = realToFrac $ unsafePerformIO $
+    withForeignPtr d $ \dp -> 
+    c_cuddCountPath dp
+
+printDebug :: DDManager -> DDNode -> Int -> Int -> IO Int
+printDebug (DDManager m) (DDNode d) n pr = liftM fromIntegral $ 
+    withForeignPtr d $ \dp -> 
+    c_cuddPrintDebug m dp (fromIntegral n) (fromIntegral pr)
+
+andAbstract :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode  
+andAbstract = cuddArg3 c_cuddBddAndAbstract
+
+xorExistAbstract :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode  
+xorExistAbstract = cuddArg3 c_cuddBddXorExistAbstract
+
+transfer :: DDManager -> DDManager -> DDNode -> DDNode
+transfer (DDManager m1) (DDManager m2) (DDNode x) = DDNode $ unsafePerformIO $ 
+    withForeignPtr x $ \xp -> do
+        node <- c_cuddBddTransfer m1 m2 xp
+        newForeignPtrEnv deref m2 node
+
+makePrime :: DDManager -> DDNode -> DDNode -> DDNode
+makePrime = cuddArg2 c_cuddBddMakePrime
+
+constrain :: DDManager -> DDNode -> DDNode -> DDNode
+constrain = cuddArg2 c_cuddBddConstrain
+
+restrict :: DDManager -> DDNode -> DDNode -> DDNode
+restrict = cuddArg2 c_cuddBddRestrict
+
+squeeze :: DDManager -> DDNode -> DDNode -> DDNode
+squeeze = cuddArg2 c_cuddBddSqueeze
+
+largestCube :: DDManager -> DDNode -> (Int, DDNode)
+largestCube (DDManager m) (DDNode n) = unsafePerformIO $ 
+    alloca $ \lp ->
+    withForeignPtr n $ \np -> do
+    node <- c_cuddLargestCube m np lp
+    res <- newForeignPtrEnv deref m node
+    l <- peek lp
+    return (fromIntegral l, DDNode res)
+     
+lEq :: DDManager -> DDNode -> DDNode -> Bool
+lEq (DDManager m) (DDNode l) (DDNode r) = (==1) $ unsafePerformIO $ 
+    withForeignPtr l $ \lp -> 
+    withForeignPtr r $ \rp ->
+    c_cuddBddLeq m lp rp
+
+ddNodeToInt :: Integral i => DDNode -> i
+ddNodeToInt = fromIntegral . ptrToIntPtr . unsafeForeignPtrToPtr . unDDNode 
+
diff --git a/Cudd/File.chs b/Cudd/File.chs
new file mode 100644
--- /dev/null
+++ b/Cudd/File.chs
@@ -0,0 +1,72 @@
+{-# LANGUAGE ForeignFunctionInterface, CPP, FlexibleContexts, RankNTypes #-}
+
+module Cudd.File (
+    DddmpVarInfoType(..),
+    DddmpMode(..),
+    DddmpVarMatchType(..),
+    cuddBddStore,
+    cuddBddLoad
+    ) where
+
+import Foreign.Storable
+import Foreign.Ptr
+import Foreign.C.Types
+import Foreign.C.String
+import Foreign.ForeignPtr
+import Foreign.Marshal.Array
+import Control.Monad
+
+import Cudd.Cudd
+import Cudd.C
+
+#include "dddmp.h"
+
+{#enum Dddmp_VarInfoType as DddmpVarInfoType {underscoreToCase} #}
+
+--Hard coded values are needed because of limitations of c2hs
+#c
+
+enum DddmpMode {
+    DddmpModeText    = 65,
+    DddmpModeBinary  = 66,
+    DddmpModeDefault = 68
+};
+
+#endc
+
+{#enum DddmpMode {} #}
+
+foreign import ccall safe "Dddmp_cuddBddStore"
+    c_dddmpBddStore :: Ptr CDDManager -> CString -> Ptr CDDNode -> Ptr CString -> Ptr CInt -> CInt -> CInt -> CString -> Ptr CFile -> IO CInt
+
+nullOnEmpty :: Storable a => [a] -> (Ptr a -> IO b) -> IO b
+nullOnEmpty lst act = 
+    case lst of
+        [] -> act nullPtr
+        _  -> withArray lst act
+
+cuddBddStore :: DDManager -> String -> DDNode -> [Int] -> DddmpMode -> DddmpVarInfoType -> String -> IO Bool
+cuddBddStore (DDManager m) name (DDNode node) auxids mode varinfo fname = liftM (/= 0) $ 
+    withCString name                      $ \pname ->
+    withForeignPtr node                   $ \dp ->
+    nullOnEmpty (map fromIntegral auxids) $ \pauxids -> 
+    withCString fname                     $ \pfname -> 
+        c_dddmpBddStore m pname dp nullPtr pauxids (fromIntegral $ fromEnum mode) (fromIntegral $ fromEnum varinfo) pfname nullPtr
+
+{#enum Dddmp_VarMatchType as DddmpVarMatchType {underscoreToCase} #}
+
+foreign import ccall safe "Dddmp_cuddBddLoad_s"
+    c_dddmpBddLoad :: Ptr CDDManager -> CInt -> Ptr CString -> Ptr CInt -> Ptr CInt -> CInt -> CString -> Ptr CFile -> IO (Ptr CDDNode)
+
+cuddBddLoad :: DDManager -> DddmpVarMatchType -> [Int] -> [Int] -> DddmpMode -> String -> IO (Maybe DDNode)
+cuddBddLoad (DDManager m) matchtype auxids composeids mode fname = 
+    nullOnEmpty (map fromIntegral auxids)     $ \pauxids -> 
+    nullOnEmpty (map fromIntegral composeids) $ \pcomposeids -> 
+    withCString fname                         $ \pfname -> do
+        node <- c_dddmpBddLoad m (fromIntegral $ fromEnum matchtype) nullPtr pauxids pcomposeids (fromIntegral $ fromEnum mode) pfname nullPtr
+        case node == nullPtr of
+            True  -> return Nothing
+            False -> do
+                fp <- newForeignPtrEnv deref m node
+                return $ Just $ DDNode fp
+
diff --git a/Cudd/ForeignHelpers.hs b/Cudd/ForeignHelpers.hs
new file mode 100644
--- /dev/null
+++ b/Cudd/ForeignHelpers.hs
@@ -0,0 +1,37 @@
+module Cudd.ForeignHelpers (
+    withForeignArray,
+    withForeignArrayPtr,
+    withForeignArrayPtrLen,
+    withStringArray,
+    withStringArrayPtr
+    ) where
+
+import Foreign
+import Foreign.C.String
+import Foreign.ForeignPtr.Unsafe
+
+withForeignArray :: [ForeignPtr a] -> ([Ptr a] -> IO b) -> IO b
+withForeignArray [] func = func []
+withForeignArray (p:ptrs) func = withForeignPtr p $ \ptr -> 
+    withForeignArray ptrs $ \x -> func (ptr:x)
+
+withForeignArray' :: [ForeignPtr a] -> ([Ptr a] -> IO b) -> IO b
+withForeignArray' ptrs io = do
+    r <- io (map unsafeForeignPtrToPtr ptrs)
+    mapM touchForeignPtr ptrs
+    return r
+
+withForeignArrayPtr :: [ForeignPtr a] -> (Ptr (Ptr a) -> IO b) -> IO b
+withForeignArrayPtr fps func = withForeignArray fps $ \ap -> withArray ap func
+
+withForeignArrayPtrLen :: [ForeignPtr a] -> (Int -> Ptr (Ptr a) -> IO b) -> IO b
+withForeignArrayPtrLen fps func = withForeignArray fps $ \ap -> withArrayLen ap func
+
+withStringArray :: [String] -> ([CString] -> IO a) -> IO a
+withStringArray [] func = func []
+withStringArray (s:strings) func = withCString s $ \ptr -> 
+    withStringArray strings $ \x -> func (ptr : x)
+
+withStringArrayPtr :: [String] -> (Ptr CString -> IO a) -> IO a
+withStringArrayPtr strings func = withStringArray strings $ \sp -> withArray sp func
+
diff --git a/Cudd/GC.hs b/Cudd/GC.hs
new file mode 100644
--- /dev/null
+++ b/Cudd/GC.hs
@@ -0,0 +1,56 @@
+{-#LANGUAGE ForeignFunctionInterface #-}
+
+module Cudd.GC (
+    cuddEnableGarbageCollection,
+    cuddDisableGarbageCollection,
+    cuddGarbageCollectionEnabled,
+    c_preGCHook_sample,
+    c_postGCHook_sample,
+    regPreGCHook,
+    regPostGCHook
+    ) where
+
+import System.IO
+import Foreign
+import Foreign.Ptr
+import Foreign.C.Types
+import Foreign.C.String
+import Foreign.ForeignPtr
+import Control.Monad
+import Control.Monad.ST
+import Control.Monad.ST.Unsafe
+
+import Cudd.Hook
+import Cudd.C
+import Cudd.Imperative
+
+foreign import ccall safe "Cudd_EnableGarbageCollection"
+	c_cuddEnableGarbageCollection :: Ptr CDDManager -> IO ()
+
+cuddEnableGarbageCollection :: DDManager s u -> ST s ()
+cuddEnableGarbageCollection (DDManager m) = unsafeIOToST $ c_cuddEnableGarbageCollection m
+
+foreign import ccall safe "Cudd_DisableGarbageCollection"
+	c_cuddDisableGarbageCollection :: Ptr CDDManager -> IO ()
+
+cuddDisableGarbageCollection :: DDManager s u -> ST s ()
+cuddDisableGarbageCollection (DDManager m) = unsafeIOToST $ c_cuddDisableGarbageCollection m
+
+foreign import ccall safe "Cudd_GarbageCollectionEnabled"
+	c_cuddGarbageCollectionEnabled :: Ptr CDDManager -> IO CInt
+
+cuddGarbageCollectionEnabled :: DDManager s u -> ST s Int
+cuddGarbageCollectionEnabled (DDManager m) = unsafeIOToST $ liftM fromIntegral $ c_cuddGarbageCollectionEnabled m
+
+foreign import ccall safe "&preGCHook_sample"
+	c_preGCHook_sample :: HookFP
+
+foreign import ccall safe "&postGCHook_sample"
+	c_postGCHook_sample :: HookFP
+
+regPreGCHook :: DDManager s u -> HookFP -> ST s Int
+regPreGCHook m func = cuddAddHook m func CuddPreGcHook
+
+regPostGCHook :: DDManager s u -> HookFP -> ST s Int
+regPostGCHook m func = cuddAddHook m func CuddPostGcHook
+
diff --git a/Cudd/Hook.chs b/Cudd/Hook.chs
new file mode 100644
--- /dev/null
+++ b/Cudd/Hook.chs
@@ -0,0 +1,42 @@
+{-#LANGUAGE ForeignFunctionInterface #-}
+
+module Cudd.Hook (
+    cuddAddHook,
+    cuddRemoveHook,
+    HookTyp,
+    HookFP,
+    CuddHookType(..)
+    ) where
+
+import System.IO
+import Foreign
+import Foreign.Ptr
+import Foreign.C.Types
+import Foreign.C.String
+import Foreign.ForeignPtr
+import Control.Monad
+import Control.Monad.ST
+import Control.Monad.ST.Unsafe
+
+import Cudd.C
+import Cudd.Imperative
+
+#include <stdio.h>
+#include <cudd.h>
+
+{#enum Cudd_HookType as CuddHookType {underscoreToCase} deriving (Show, Eq) #}
+
+type HookTyp = Ptr CDDManager -> CString -> Ptr () -> IO (CInt)
+type HookFP  = FunPtr HookTyp
+
+foreign import ccall safe "Cudd_AddHook"
+	c_cuddAddHook :: Ptr CDDManager -> HookFP -> CInt -> IO (CInt)
+
+cuddAddHook :: DDManager s u -> HookFP -> CuddHookType -> ST s Int
+cuddAddHook (DDManager m) fp typ = unsafeIOToST $ liftM fromIntegral $ c_cuddAddHook m fp (fromIntegral $ fromEnum typ)
+	
+foreign import ccall safe "Cudd_RemoveHook"
+	c_cuddRemoveHook :: Ptr CDDManager -> HookFP -> CInt -> IO (CInt)
+
+cuddRemoveHook :: DDManager s u -> HookFP -> CuddHookType -> ST s Int
+cuddRemoveHook (DDManager m) fp typ = unsafeIOToST $ liftM fromIntegral $ c_cuddRemoveHook m fp (fromIntegral $ fromEnum typ)
diff --git a/Cudd/Imperative.hs b/Cudd/Imperative.hs
new file mode 100644
--- /dev/null
+++ b/Cudd/Imperative.hs
@@ -0,0 +1,430 @@
+{-# LANGUAGE RankNTypes #-}
+
+module Cudd.Imperative (
+    DDManager(..),
+    DDNode(..),
+    cuddInit,
+    cuddInitDefaults,
+    withManager, 
+    withManagerDefaults,
+    withManagerIO,
+    withManagerIODefaults,
+    shuffleHeap,
+    bZero,
+    bOne,
+    ithVar,
+    bAnd,
+    bOr,
+    bNand,
+    bNor,
+    bXor,
+    bXnor,
+    bNot,
+    bIte,
+    bExists,
+    bForall,
+    deref,
+    setVarMap,
+    varMap,
+    lEq,
+    swapVariables,
+    ref,
+    largestCube,
+    makePrime,
+    support,
+    supportIndices,
+    indicesToCube,
+    computeCube,
+    nodesToCube,
+    readSize,
+    bddToCubeArray,
+    compose,
+    andAbstract,
+    xorExistAbstract,
+    leqUnless,
+    equivDC,
+    xEqY,
+    debugCheck,
+    checkKeys,
+    pickOneMinterm,
+    toInt,
+    checkZeroRef,
+    readInvPerm,
+    readPerm,
+    dagSize,
+    readNodeCount,
+    readPeakNodeCount,
+    regular,
+    readMaxCache,
+    readMaxCacheHard,
+    setMaxCacheHard,
+    readCacheSlots,
+    readCacheUsedSlots,
+    cudd_unique_slots,
+    cudd_cache_slots,
+    andLimit,
+    readTree,
+    newVarAtLevel,
+    liCompaction,
+    squeeze,
+    minimize,
+    newVar,
+    vectorCompose,
+    quit,
+    readIndex,
+    printMinterm,
+    checkCube,
+    Cube,
+    Prime,
+    DDGen(..),
+    genFree,
+    isGenEmpty,
+    firstCube,
+    nextCube,
+    firstPrime,
+    nextPrime,
+    module Cudd.Common
+    ) where
+
+import Foreign hiding (void)
+import Foreign.Ptr
+import Foreign.C.Types
+import Control.Monad.ST
+import Control.Monad.ST.Unsafe
+import Control.Monad
+import Control.Monad.IO.Class
+import Data.List
+import System.IO.Unsafe
+
+import Cudd.C
+import Cudd.MTR
+import Cudd.Common
+
+newtype DDManager s u = DDManager {unDDManager :: Ptr CDDManager}
+newtype DDNode    s u = DDNode    {unDDNode    :: Ptr CDDNode} deriving (Ord, Eq, Show)
+
+cuddInit :: Int -> Int -> Int -> Int -> Int -> ST s (DDManager s u)
+cuddInit numVars numVarsZ numSlots cacheSize maxMemory = unsafeIOToST $ do
+    cm <- c_cuddInit (fromIntegral numVars) (fromIntegral numVarsZ) (fromIntegral numSlots) (fromIntegral cacheSize) (fromIntegral maxMemory)
+    return $ DDManager cm
+
+cuddInitDefaults :: ST s (DDManager s u)
+cuddInitDefaults = cuddInit 0 0 cudd_unique_slots cudd_cache_slots 0
+
+withManager :: Int -> Int -> Int -> Int -> Int -> (forall u. DDManager s u -> ST s a) -> ST s a
+withManager numVars numVarsZ numSlots cacheSize maxMemory f = do
+    res <- cuddInit numVars numVarsZ numSlots cacheSize maxMemory
+    f res 
+
+withManagerDefaults :: (forall u. DDManager s u -> ST s a) -> ST s a
+withManagerDefaults f = do
+    res <- cuddInitDefaults
+    f res 
+
+withManagerIO :: MonadIO m => Int -> Int -> Int -> Int -> Int -> (forall u. DDManager RealWorld u -> m a) -> m a
+withManagerIO numVars numVarsZ numSlots cacheSize maxMemory f = do
+    res <- liftIO $ stToIO $ cuddInit numVars numVarsZ numSlots cacheSize maxMemory
+    f res
+
+withManagerIODefaults :: MonadIO m => (forall u. DDManager RealWorld u -> m a) -> m a
+withManagerIODefaults f = do
+    res <- liftIO $ stToIO cuddInitDefaults
+    f res
+
+shuffleHeap :: DDManager s u -> [Int] -> ST s ()
+shuffleHeap (DDManager m) order = unsafeIOToST $ 
+    withArrayLen (map fromIntegral order) $ \size ptr -> do
+    when (sort order /= [0..size-1]) (error "shuffleHeap: order does not contain each variable once") 
+    res1 <- c_cuddBddIthVar m (fromIntegral (size - 1))
+    when (res1 == nullPtr) (error "shuffleHeap: Failed to resize table")
+    res2 <- c_cuddShuffleHeap m ptr
+    when (fromIntegral res2 /= 1) (error "shuffleHeap: Cudd_ShuffleHeap failed")
+    return ()
+
+toInt :: DDNode s u -> Int
+toInt (DDNode n) = fromIntegral $ ptrToIntPtr n
+
+arg0 :: (Ptr CDDManager -> IO (Ptr CDDNode)) -> DDManager s u -> ST s (DDNode s u)
+arg0 f (DDManager m) = liftM DDNode $ unsafeIOToST $ f m
+
+arg1 :: (Ptr CDDManager -> Ptr CDDNode -> IO (Ptr CDDNode)) -> DDManager s u -> DDNode s u -> ST s (DDNode s u)
+arg1 f (DDManager m) (DDNode x) = liftM DDNode $ unsafeIOToST $ f m x
+
+arg2 :: (Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)) -> DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)
+arg2 f (DDManager m) (DDNode x) (DDNode y) = liftM DDNode $ unsafeIOToST $ f m x y
+    
+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 (DDManager m) = DDNode $ unsafePerformIO $ c_cuddReadLogicZero m
+bOne  (DDManager m) = DDNode $ unsafePerformIO $ c_cuddReadOne m
+
+bAnd    = arg2 c_cuddBddAnd
+bOr     = arg2 c_cuddBddOr
+bNand   = arg2 c_cuddBddNand
+bNor    = arg2 c_cuddBddNor
+bXor    = arg2 c_cuddBddXor
+bXnor   = arg2 c_cuddBddXnor
+bIte    = arg3 c_cuddBddIte
+bExists = arg2 c_cuddBddExistAbstract
+bForall = arg2 c_cuddBddUnivAbstract
+
+andAbstract      = arg3 c_cuddBddAndAbstract
+xorExistAbstract = arg3 c_cuddBddXorExistAbstract
+
+bNot (DDNode x) = DDNode $ unsafePerformIO $ c_cuddNotNoRef x
+ithVar (DDManager m) i = liftM DDNode $ unsafeIOToST $ c_cuddBddIthVar m (fromIntegral i)
+
+deref :: DDManager s u -> DDNode s u -> ST s ()
+deref (DDManager m) (DDNode x) = unsafeIOToST $ c_cuddIterDerefBdd m x
+
+setVarMap :: DDManager s u -> [DDNode s u] -> [DDNode s u] -> ST s ()
+setVarMap (DDManager m) xs ys = unsafeIOToST $ 
+    withArrayLen (map unDDNode xs) $ \xl xp -> 
+    withArrayLen (map unDDNode ys) $ \yl yp -> do
+    when (xl /= yl) (error "setVarMap: lengths not equal")
+    void $ c_cuddSetVarMap m xp yp (fromIntegral xl)
+
+varMap :: DDManager s u -> DDNode s u -> ST s (DDNode s u)
+varMap (DDManager m) (DDNode x) = liftM DDNode $ unsafeIOToST $ c_cuddBddVarMap m x
+
+lEq :: DDManager s u -> DDNode s u -> DDNode s u -> ST s Bool
+lEq (DDManager m) (DDNode x) (DDNode y) = liftM (==1) $ unsafeIOToST $ c_cuddBddLeq m x y
+
+swapVariables :: DDManager s u -> [DDNode s u] -> [DDNode s u] -> DDNode s u -> ST s (DDNode s u)
+swapVariables (DDManager m) nodesx nodesy (DDNode x) = unsafeIOToST $ 
+    withArrayLen (map unDDNode nodesx) $ \lx xp -> 
+    withArrayLen (map unDDNode nodesy) $ \ly yp -> do
+    when (lx /= ly) $ error "CuddExplicitDeref: shift: lengths not equal"
+    res <- c_cuddBddSwapVariables m x xp yp (fromIntegral lx)
+    return $ DDNode res
+
+ref :: DDNode s u -> ST s ()
+ref (DDNode x) = unsafeIOToST $ cuddRef x
+
+largestCube :: DDManager s u -> DDNode s u -> ST s (DDNode s u, Int)
+largestCube (DDManager m) (DDNode x) = unsafeIOToST $ 
+    alloca $ \lp -> do
+    res <- c_cuddLargestCube m x lp 
+    l <- peek lp
+    return (DDNode res, fromIntegral l)
+
+makePrime :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)
+makePrime = arg2 c_cuddBddMakePrime
+
+support :: DDManager s u -> DDNode s u -> ST s (DDNode s u)
+support = arg1 c_cuddSupport
+
+supportIndices :: DDManager s u -> DDNode s u -> ST s [Int]
+supportIndices (DDManager m) (DDNode x) = unsafeIOToST $
+    alloca $ \arrp -> do
+    sz <- c_cuddSupportIndices m x arrp
+    aaddr <- peek arrp
+    res <- peekArray (fromIntegral sz) aaddr
+    return $ map fromIntegral res
+
+indicesToCube :: DDManager s u -> [Int] -> ST s (DDNode s u)
+indicesToCube (DDManager m) indices = unsafeIOToST $
+    withArrayLen (map fromIntegral indices) $ \sz pt -> do
+    res <- c_cuddIndicesToCube m pt (fromIntegral sz)
+    return $ DDNode res
+
+computeCube :: DDManager s u -> [DDNode s u] -> [Bool] -> ST s (DDNode s u)
+computeCube (DDManager m) nodes phases = unsafeIOToST $ 
+    withArrayLen (map unDDNode nodes) $ \szn ptn -> 
+    withArrayLen (map (fromIntegral . fromBool) phases) $ \szp ptp -> do
+    when (szn /= szp) $ error "computeCube: lists are different lengths"
+    res <- c_cuddBddComputeCube m ptn ptp (fromIntegral szn)
+    return $ DDNode res
+
+nodesToCube :: DDManager s u -> [DDNode s u] -> ST s (DDNode s u)
+nodesToCube (DDManager m) nodes = unsafeIOToST $
+    withArrayLen (map unDDNode nodes) $ \sz pt -> do
+    res <- c_cuddBddComputeCube m pt nullPtr (fromIntegral sz)
+    return $ DDNode res
+
+readSize :: DDManager s u -> ST s Int
+readSize (DDManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadSize m
+
+bddToCubeArray :: DDManager s u -> DDNode s u -> ST s [SatBit]
+bddToCubeArray ma@(DDManager m) (DDNode x) = unsafeIOToST $ do
+    size <- liftM fromIntegral $ c_cuddReadSize m
+    allocaArray size $ \resptr -> do
+        c_cuddBddToCubeArray m x resptr
+        res <- peekArray size resptr
+        return $ map (toSatBit . fromIntegral) res
+
+compose :: DDManager s u -> DDNode s u -> DDNode s u -> Int -> ST s (DDNode s u)
+compose (DDManager m) (DDNode f) (DDNode g) v = liftM DDNode $ unsafeIOToST $ c_cuddBddCompose m f g (fromIntegral v)
+
+arg3Bool :: (Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO CInt) -> DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u  -> ST s Bool
+arg3Bool f (DDManager m) (DDNode x) (DDNode y) (DDNode z) = liftM (==1) $ unsafeIOToST $ f m x y z
+
+leqUnless, equivDC :: DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s Bool
+leqUnless = arg3Bool c_cuddBddLeqUnless
+equivDC   = arg3Bool c_cuddEquivDC
+
+xEqY :: DDManager s u -> [DDNode s u] -> [DDNode s u] -> ST s (DDNode s u)
+xEqY (DDManager m) xs ys = unsafeIOToST $ 
+    withArrayLen (map unDDNode xs) $ \xl xp -> 
+    withArrayLen (map unDDNode ys) $ \yl yp -> do
+    when (xl /= yl) (error "xeqy: lengths not equal")
+    res <- c_cuddXeqy m (fromIntegral xl) xp yp
+    return $ DDNode res
+
+debugCheck :: DDManager s u -> ST s Int
+debugCheck (DDManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddDebugCheck m
+
+checkKeys :: DDManager s u -> ST s Int
+checkKeys (DDManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddCheckKeys m
+
+pickOneMinterm :: DDManager s u -> DDNode s u -> [DDNode s u] -> ST s (DDNode s u)
+pickOneMinterm (DDManager m) (DDNode d) vars = unsafeIOToST $ 
+    withArrayLen (map unDDNode vars) $ \vl vp -> do
+        res <- c_cuddBddPickOneMinterm m d vp (fromIntegral vl)
+        return $ DDNode res
+
+checkZeroRef :: DDManager s u -> ST s Int
+checkZeroRef (DDManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddCheckZeroRef m
+
+readInvPerm :: DDManager s u -> Int -> ST s Int
+readInvPerm (DDManager m) offs = liftM fromIntegral $ unsafeIOToST $ c_cuddReadInvPerm m (fromIntegral offs)
+
+readPerm :: DDManager s u -> Int -> ST s Int
+readPerm (DDManager m) offs = liftM fromIntegral $ unsafeIOToST $ c_cuddReadPerm m (fromIntegral offs)
+
+dagSize :: DDNode s u -> ST s Int
+dagSize (DDNode d) = liftM fromIntegral $ unsafeIOToST $ c_cuddDagSize d
+
+readNodeCount :: DDManager s u -> ST s Integer
+readNodeCount (DDManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadNodeCount m
+
+readPeakNodeCount :: DDManager s u -> ST s Integer
+readPeakNodeCount (DDManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadPeakNodeCount m
+
+regular :: DDNode s u -> DDNode s u
+regular (DDNode x) = DDNode $ unsafePerformIO $ c_wrappedRegular x
+
+readMaxCache :: DDManager s u -> ST s Int
+readMaxCache (DDManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadMaxCache m
+
+readMaxCacheHard :: DDManager s u -> ST s Int
+readMaxCacheHard (DDManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadMaxCacheHard m
+
+setMaxCacheHard :: DDManager s u -> Int -> ST s ()
+setMaxCacheHard (DDManager m) x = unsafeIOToST $ c_cuddSetMaxCacheHard m (fromIntegral x)
+
+readCacheSlots :: DDManager s u -> ST s Int
+readCacheSlots (DDManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadCacheSlots m
+
+readCacheUsedSlots :: DDManager s u -> ST s Int
+readCacheUsedSlots (DDManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadCacheUsedSlots m
+
+andLimit :: DDManager s u -> DDNode s u -> DDNode s u -> Int -> ST s (Maybe (DDNode s u))
+andLimit (DDManager m) (DDNode x) (DDNode y) lim = unsafeIOToST $ do
+    res <- c_cuddBddAndLimit m x y (fromIntegral lim)
+    if res==nullPtr then
+        return Nothing
+    else do
+        cuddRef res
+        return $ Just $ DDNode res
+
+readTree :: DDManager s u -> ST s (MtrNode s)
+readTree (DDManager m) = liftM MtrNode $ unsafeIOToST $ c_cuddReadTree m
+
+newVarAtLevel :: DDManager s u -> Int -> ST s (DDNode s u)
+newVarAtLevel (DDManager m) level = liftM DDNode $ unsafeIOToST $ c_cuddBddNewVarAtLevel m (fromIntegral level)
+
+liCompaction = arg2 c_cuddBddLICompaction
+squeeze      = arg2 c_cuddBddSqueeze
+minimize     = arg2 c_cuddBddMinimize
+
+newVar :: DDManager s u -> ST s (DDNode s u)
+newVar (DDManager m) = liftM DDNode $ unsafeIOToST $ c_cuddBddNewVar m
+
+vectorCompose :: DDManager s u -> DDNode s u -> [DDNode s u] -> ST s (DDNode s u)
+vectorCompose (DDManager m) (DDNode f) nodes = liftM DDNode $ unsafeIOToST $ withArrayLen (map unDDNode nodes) $ \len ptr -> do
+    sz <- c_cuddReadSize m
+    when (fromIntegral sz /= len) (error "vectorCompose: not one entry for each variable in manager")
+    c_cuddBddVectorCompose m f ptr
+
+quit :: DDManager s u -> ST s ()
+quit (DDManager m) = unsafeIOToST $ c_cuddQuit m
+
+readIndex :: DDNode s u -> ST s Int
+readIndex (DDNode x) = liftM fromIntegral $ unsafeIOToST $ c_cuddNodeReadIndex x
+
+printMinterm :: DDManager s u -> DDNode s u -> ST s ()
+printMinterm (DDManager m) (DDNode x) = unsafeIOToST $ c_cuddPrintMinterm m x
+
+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 DDGen s u t = DDGen (Ptr CDDGen)
+
+genFree :: DDGen s u t -> ST s ()
+genFree (DDGen g) = void $ unsafeIOToST $ c_cuddGenFree g
+
+isGenEmpty :: DDGen s u t -> ST s Bool
+isGenEmpty (DDGen g) = liftM (==1) $ unsafeIOToST $ c_cuddIsGenEmpty g
+
+firstCube :: DDManager s u -> DDNode s u -> ST s (Maybe ([SatBit], DDGen s u Cube))
+firstCube (DDManager m) (DDNode n) = unsafeIOToST $ do
+    sz <- c_cuddReadSize m
+    alloca $ \cubePP -> 
+        alloca $ \valP -> do
+            gen <- c_cuddFirstCube m n cubePP valP 
+            empty <- c_cuddIsGenEmpty gen
+            if empty == 1 then do
+                c_cuddGenFree gen
+                return Nothing
+            else do
+                cubeP <- peek cubePP
+                cube <- peekArray (fromIntegral sz) cubeP
+                return $ Just (map (toSatBit . fromIntegral) cube, DDGen gen)
+
+nextCube :: DDManager s u -> DDGen s u Cube -> ST s (Maybe [SatBit])
+nextCube (DDManager m) (DDGen g) = unsafeIOToST $ do
+    sz <- c_cuddReadSize m
+    alloca $ \cubePP -> 
+        alloca $ \valP -> do
+            c_cuddNextCube g cubePP valP
+            empty <- c_cuddIsGenEmpty g
+            if empty == 1 then do
+                c_cuddGenFree g
+                return Nothing
+            else do
+                cubeP <- peek cubePP
+                cube <- peekArray (fromIntegral sz) cubeP
+                return $ Just $ map (toSatBit . fromIntegral) cube
+
+firstPrime :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (Maybe ([SatBit], DDGen s u Prime))
+firstPrime (DDManager m) (DDNode x) (DDNode y) = unsafeIOToST $ do
+    sz <- c_cuddReadSize m
+    alloca $ \cubePP -> do
+        gen <- c_cuddFirstPrime m x y cubePP
+        empty <- c_cuddIsGenEmpty gen
+        if empty == 1 then do
+            c_cuddGenFree gen
+            return Nothing
+        else do
+            cubeP <- peek cubePP
+            cube <- peekArray (fromIntegral sz) cubeP
+            return $ Just (map (toSatBit . fromIntegral) cube, DDGen gen)
+
+nextPrime :: DDManager s u -> DDGen s u Prime -> ST s (Maybe [SatBit])
+nextPrime (DDManager m) (DDGen g) = unsafeIOToST $ do
+    sz <- c_cuddReadSize m
+    alloca $ \cubePP -> do
+        c_cuddNextPrime g cubePP 
+        empty <- c_cuddIsGenEmpty g
+        if empty == 1 then do
+            c_cuddGenFree g
+            return Nothing
+        else do
+            cubeP <- peek cubePP
+            cube <- peekArray (fromIntegral sz) cubeP
+            return $ Just $ map (toSatBit . fromIntegral) cube
+
diff --git a/Cudd/MTR.chs b/Cudd/MTR.chs
new file mode 100644
--- /dev/null
+++ b/Cudd/MTR.chs
@@ -0,0 +1,125 @@
+{-# LANGUAGE ForeignFunctionInterface, EmptyDataDecls, CPP #-}
+
+module Cudd.MTR (
+    MtrNode(..),
+    CMtrNode,
+    mtrAllocNode,
+    mtrCreateFirstChild,
+    mtrCreateLastChild,
+    mtrDeallocNode,
+    mtrMakeFirstChild,
+    mtrMakeLastChild,
+    mtrMakeNextSibling,
+    mtrPrintGroups,
+    mtrPrintTree,
+    mtrMakeGroup,
+    mtrInitGroupTree,
+    mtrFindGroup,
+    mtrDissolveGroup,
+    MTRType(..)
+    ) where
+
+import System.IO
+import Foreign
+import Foreign.Ptr
+import Foreign.C.Types
+import Control.Monad
+import Control.Monad.ST
+import Control.Monad.ST.Unsafe
+
+#include <stdio.h>
+#include <mtr.h>
+
+data CMtrNode 
+newtype MtrNode s = MtrNode (Ptr CMtrNode)
+
+foreign import ccall unsafe "Mtr_AllocNode"
+    c_mtrAllocNode :: IO (Ptr CMtrNode)
+
+mtrAllocNode :: ST s (MtrNode s) 
+mtrAllocNode = liftM MtrNode $ unsafeIOToST c_mtrAllocNode
+
+foreign import ccall unsafe "Mtr_CreateFirstChild"
+    c_mtrCreateFirstChild :: Ptr CMtrNode -> IO (Ptr CMtrNode)
+
+mtrCreateFirstChild :: MtrNode s -> ST s (MtrNode s)
+mtrCreateFirstChild (MtrNode p) = liftM MtrNode $ unsafeIOToST $ c_mtrCreateFirstChild p
+
+foreign import ccall unsafe "Mtr_CreateLastChild"
+    c_mtrCreateLastChild :: Ptr CMtrNode -> IO (Ptr CMtrNode)
+
+mtrCreateLastChild :: MtrNode s -> ST s (MtrNode s)
+mtrCreateLastChild (MtrNode p) = liftM MtrNode $ unsafeIOToST $ c_mtrCreateLastChild p
+
+foreign import ccall unsafe "Mtr_DeallocNode"
+    c_mtrDeallocNode :: Ptr CMtrNode -> IO ()
+
+mtrDeallocNode :: MtrNode s -> ST s ()
+mtrDeallocNode (MtrNode p) = unsafeIOToST $ c_mtrDeallocNode p
+
+foreign import ccall unsafe "Mtr_MakeFirstChild"
+    c_mtrMakeFirstChild :: Ptr CMtrNode -> Ptr CMtrNode -> IO ()
+
+mtrMakeFirstChild :: MtrNode s -> MtrNode s -> ST s ()
+mtrMakeFirstChild (MtrNode p) (MtrNode c) = unsafeIOToST $ c_mtrMakeFirstChild p c
+
+foreign import ccall unsafe "Mtr_MakeLastChild"
+    c_mtrMakeLastChild :: Ptr CMtrNode -> Ptr CMtrNode -> IO ()
+
+mtrMakeLastChild :: MtrNode s -> MtrNode s -> ST s ()
+mtrMakeLastChild (MtrNode p) (MtrNode c) = unsafeIOToST $ c_mtrMakeLastChild p c
+
+foreign import ccall unsafe "Mtr_MakeNextSibling"
+    c_mtrMakeNextSibling :: Ptr CMtrNode -> Ptr CMtrNode -> IO ()
+
+mtrMakeNextSibling :: MtrNode s -> MtrNode s -> ST s ()
+mtrMakeNextSibling (MtrNode f) (MtrNode s) = unsafeIOToST $ c_mtrMakeNextSibling f s
+
+foreign import ccall unsafe "Mtr_PrintGroups"
+    c_mtrPrintGroups :: Ptr CMtrNode -> CInt -> IO ()
+
+mtrPrintGroups :: MtrNode s -> Int -> ST s ()
+mtrPrintGroups (MtrNode c) s = unsafeIOToST $ c_mtrPrintGroups c (fromIntegral s)
+
+foreign import ccall unsafe "Mtr_PrintTree"
+    c_mtrPrintTree :: Ptr CMtrNode -> IO ()
+
+mtrPrintTree :: MtrNode s -> ST s ()
+mtrPrintTree (MtrNode c) = unsafeIOToST $ c_mtrPrintTree c
+
+foreign import ccall unsafe "Mtr_MakeGroup"
+    c_mtrMakeGroup :: Ptr CMtrNode -> CInt -> CInt -> CInt -> IO (Ptr CMtrNode)
+
+mtrMakeGroup :: MtrNode s -> Int -> Int -> Int -> ST s (MtrNode s)
+mtrMakeGroup (MtrNode r) l s f = liftM MtrNode $ unsafeIOToST $ c_mtrMakeGroup r (fromIntegral l) (fromIntegral s) (fromIntegral f)
+
+foreign import ccall unsafe "Mtr_InitGroupTree"
+    c_mtrInitGroupTree :: CInt -> CInt -> IO (Ptr CMtrNode)
+
+mtrInitGroupTree :: Int -> Int -> ST s (MtrNode s)
+mtrInitGroupTree l s = liftM MtrNode $ unsafeIOToST $ c_mtrInitGroupTree (fromIntegral l) (fromIntegral s)
+
+foreign import ccall unsafe "Mtr_FindGroup"
+    c_mtrFindGroup :: Ptr CMtrNode -> CUInt -> CUInt -> IO (Ptr CMtrNode)
+
+mtrFindGroup :: MtrNode s -> Int -> Int -> ST s (MtrNode s)
+mtrFindGroup (MtrNode m) x y = liftM MtrNode $ unsafeIOToST $ c_mtrFindGroup m (fromIntegral x) (fromIntegral y)
+
+foreign import ccall unsafe "Mtr_DissolveGroup"
+    c_mtrDissolveGroup :: Ptr CMtrNode -> IO ()
+
+mtrDissolveGroup :: MtrNode s -> ST s ()
+mtrDissolveGroup (MtrNode m) = unsafeIOToST $ c_mtrDissolveGroup m
+
+#c
+enum MTR_TYPES {
+    MTRDefault = MTR_DEFAULT,
+    MTRTerminal = MTR_TERMINAL,
+    MTRSoft = MTR_SOFT,
+    MTRFixed = MTR_FIXED,
+    MTRNewNode = MTR_NEWNODE
+};
+#endc
+
+{#enum MTR_TYPES as MTRType {underscoreToCase} deriving (Show, Eq) #}
+
diff --git a/Cudd/Reorder.chs b/Cudd/Reorder.chs
new file mode 100644
--- /dev/null
+++ b/Cudd/Reorder.chs
@@ -0,0 +1,283 @@
+{-#LANGUAGE ForeignFunctionInterface #-}
+
+module Cudd.Reorder (
+    CuddReorderingType(..),
+    cuddReorderingStatus,
+    cuddAutodynEnable,
+    cuddAutodynDisable,
+    cuddReduceHeap,
+    cuddMakeTreeNode,
+    cuddReadReorderingTime,
+    cuddReadReorderings,
+    cuddEnableReorderingReporting,
+    cuddDisableReorderingReporting,
+    cuddReorderingReporting,
+    regStdPreReordHook,
+    regStdPostReordHook,
+    cuddTurnOnCountDead,
+    cuddTurnOffCountDead,
+    cuddDeadAreCounted,
+    cuddReadSiftMaxSwap,
+    cuddSetSiftMaxSwap,
+    cuddReadSiftMaxVar,
+    cuddSetSiftMaxVar,
+    cuddReadNextReordering,
+    cuddSetNextReordering,
+    cuddReadMaxGrowthAlternate,
+    cuddSetMaxGrowthAlternate,
+    cuddReadMaxGrowth,
+    cuddReadReorderingCycle,
+    cuddSetReorderingCycle,
+    cuddSetPopulationSize,
+    cuddReadNumberXovers,
+    cuddSetNumberXovers,
+    regReordGCHook
+    ) where
+
+import System.IO
+import System.Mem
+import Foreign
+import Foreign.Ptr
+import Foreign.C.Types
+import Foreign.C.String
+import Foreign.ForeignPtr
+import Control.Monad
+import Control.Monad.ST
+import Control.Monad.ST.Unsafe
+
+import Cudd.C
+import Cudd.Hook
+import Cudd.Imperative
+
+#include <stdio.h>
+#include <cudd.h>
+
+readIntegral :: (Integral i, Num j) => (Ptr CDDManager -> IO i) -> DDManager s u -> ST s j
+readIntegral f (DDManager m) = unsafeIOToST $ liftM fromIntegral $ f m
+
+setIntegral :: (Integral i, Num j) => (Ptr CDDManager -> j -> IO ()) -> DDManager s u -> i -> ST s ()
+setIntegral f (DDManager m) v = unsafeIOToST $ f m (fromIntegral v)
+
+readFloat :: (Real r, Fractional f) => (Ptr CDDManager -> IO r) -> DDManager s u -> ST s f
+readFloat f (DDManager m) = unsafeIOToST $ liftM realToFrac $ f m 
+
+setFloat :: (Real r, Fractional f) => (Ptr CDDManager -> f -> IO ()) -> DDManager s u -> r -> ST s ()
+setFloat f (DDManager m) v = unsafeIOToST $ f m (realToFrac v)
+
+--Reordering types
+{#enum Cudd_ReorderingType as CuddReorderingType {underscoreToCase} deriving (Show, Eq) #}
+
+--Reorder when needed
+foreign import ccall safe "Cudd_ReorderingStatus"
+	c_cuddReorderingStatus :: Ptr CDDManager -> Ptr CInt -> IO (CInt)
+
+cuddReorderingStatus :: DDManager s u -> ST s (Int, CuddReorderingType)
+cuddReorderingStatus (DDManager m) = unsafeIOToST $ do
+	alloca $ \mem -> do
+		res <- c_cuddReorderingStatus m mem
+		typ <- peek mem
+		return $ (fromIntegral res, toEnum $ fromIntegral typ)
+
+foreign import ccall safe "Cudd_AutodynEnable"
+	c_cuddAutodynEnable :: Ptr CDDManager -> CInt -> IO ()
+
+cuddAutodynEnable :: DDManager s u -> CuddReorderingType -> ST s ()
+cuddAutodynEnable (DDManager m) t = unsafeIOToST $ c_cuddAutodynEnable m (fromIntegral $ fromEnum t)
+
+foreign import ccall safe "Cudd_AutodynDisable"
+	c_cuddAutodynDisable :: Ptr CDDManager -> IO ()
+
+cuddAutodynDisable :: DDManager s u -> ST s ()
+cuddAutodynDisable (DDManager m) = unsafeIOToST $ c_cuddAutodynDisable m
+
+--Reorder right now
+foreign import ccall safe "Cudd_ReduceHeap"
+	c_cuddReduceHeap :: Ptr CDDManager -> CInt -> CInt -> IO (CInt)
+
+cuddReduceHeap :: DDManager s u -> CuddReorderingType -> Int -> ST s Int
+cuddReduceHeap (DDManager m) typ minsize = unsafeIOToST $ liftM fromIntegral $ c_cuddReduceHeap m (fromIntegral $ fromEnum typ) (fromIntegral minsize)
+
+--Grouping
+foreign import ccall safe "Cudd_MakeTreeNode"
+	c_cuddMakeTreeNode :: Ptr CDDManager -> CUInt -> CUInt -> CUInt -> IO (Ptr ())
+
+cuddMakeTreeNode :: DDManager s u -> Int -> Int -> Int -> ST s (Ptr ())
+cuddMakeTreeNode (DDManager m) low size typ = unsafeIOToST $ do
+    res <- c_cuddMakeTreeNode m (fromIntegral low) (fromIntegral size) (fromIntegral typ)
+    when (res==nullPtr) (error "cuddMakeTreeNode returned error")
+    return res
+
+--Reordering stats
+foreign import ccall safe "Cudd_ReadReorderingTime"
+	c_cuddReadReorderingTime :: Ptr CDDManager -> IO (CLong)
+
+cuddReadReorderingTime :: DDManager s u -> ST s Int
+cuddReadReorderingTime = readIntegral c_cuddReadReorderingTime
+
+foreign import ccall safe "Cudd_ReadReorderings"
+	c_cuddReadReorderings :: Ptr CDDManager -> IO (CUInt)
+
+cuddReadReorderings :: DDManager s u -> ST s Int
+cuddReadReorderings = readIntegral c_cuddReadReorderings
+
+--Hooks
+foreign import ccall safe "&Cudd_StdPreReordHook"
+	c_cuddStdPreReordHook :: HookFP
+
+foreign import ccall safe "&Cudd_StdPostReordHook"
+	c_cuddStdPostReordHook :: HookFP
+
+foreign import ccall safe "Cudd_EnableReorderingReporting"
+	c_cuddEnableReorderingReporting :: Ptr CDDManager -> IO (CInt)
+
+cuddEnableReorderingReporting :: DDManager s u -> ST s Int
+cuddEnableReorderingReporting (DDManager m) = unsafeIOToST $ liftM fromIntegral $ c_cuddEnableReorderingReporting m
+
+foreign import ccall safe "Cudd_DisableReorderingReporting"
+	c_cuddDisableReorderingReporting :: Ptr CDDManager -> IO (CInt)
+
+cuddDisableReorderingReporting :: DDManager s u -> ST s Int
+cuddDisableReorderingReporting (DDManager m) = unsafeIOToST $ liftM fromIntegral $ c_cuddDisableReorderingReporting m
+
+foreign import ccall safe "Cudd_ReorderingReporting"
+	c_cuddReorderingReporting :: Ptr CDDManager -> IO (CInt)
+
+cuddReorderingReporting :: DDManager s u -> ST s Int
+cuddReorderingReporting (DDManager m) = unsafeIOToST $ liftM fromIntegral $ c_cuddReorderingReporting m
+
+regStdPreReordHook :: DDManager s u -> ST s Int
+regStdPreReordHook m = cuddAddHook m c_cuddStdPreReordHook CuddPreReorderingHook
+
+regStdPostReordHook :: DDManager s u -> ST s Int
+regStdPostReordHook m = cuddAddHook m c_cuddStdPostReordHook CuddPostReorderingHook
+
+--Universal reordering params
+foreign import ccall safe "Cudd_TurnOffCountDead"
+	c_cuddTurnOffCountDead :: Ptr CDDManager -> IO ()
+
+cuddTurnOffCountDead :: DDManager s u -> ST s ()
+cuddTurnOffCountDead (DDManager m) = unsafeIOToST $ c_cuddTurnOffCountDead m
+
+foreign import ccall safe "Cudd_TurnOnCountDead"
+	c_cuddTurnOnCountDead :: Ptr CDDManager -> IO ()
+
+cuddTurnOnCountDead :: DDManager s u -> ST s ()
+cuddTurnOnCountDead (DDManager m) = unsafeIOToST $ c_cuddTurnOnCountDead m
+
+foreign import ccall safe "Cudd_DeadAreCounted"
+	c_cuddDeadAreCounted :: Ptr CDDManager -> IO CInt
+
+cuddDeadAreCounted :: DDManager s u -> ST s Int
+cuddDeadAreCounted (DDManager m) = unsafeIOToST $ liftM fromIntegral $ c_cuddDeadAreCounted m
+
+--Sifting parameters
+foreign import ccall safe "Cudd_ReadSiftMaxSwap"
+	c_cuddReadSiftMaxSwap :: Ptr CDDManager -> IO (CInt)
+
+cuddReadSiftMaxSwap :: DDManager s u -> ST s Int
+cuddReadSiftMaxSwap = readIntegral c_cuddReadSiftMaxSwap
+
+foreign import ccall safe "Cudd_SetSiftMaxSwap"
+	c_cuddSetSiftMaxSwap :: Ptr CDDManager -> CInt -> IO ()
+
+cuddSetSiftMaxSwap :: DDManager s u -> Int -> ST s ()
+cuddSetSiftMaxSwap = setIntegral c_cuddSetSiftMaxSwap 
+
+foreign import ccall safe "Cudd_ReadSiftMaxVar"
+	c_cuddReadSiftMaxVar :: Ptr CDDManager -> IO (Int)
+
+cuddReadSiftMaxVar :: DDManager s u -> ST s Int
+cuddReadSiftMaxVar = readIntegral c_cuddReadSiftMaxVar
+
+foreign import ccall safe "Cudd_SetSiftMaxVar"
+	c_cuddSetSiftMaxVar :: Ptr CDDManager -> CInt -> IO ()
+
+cuddSetSiftMaxVar :: DDManager s u -> Int -> ST s ()
+cuddSetSiftMaxVar = setIntegral c_cuddSetSiftMaxVar
+	
+foreign import ccall safe "Cudd_ReadNextReordering"
+	c_cuddReadNextReordering :: Ptr CDDManager -> IO (Int)
+
+cuddReadNextReordering :: DDManager s u -> ST s Int
+cuddReadNextReordering = readIntegral c_cuddReadNextReordering
+
+foreign import ccall safe "Cudd_SetNextReordering"
+	c_cuddSetNextReordering :: Ptr CDDManager -> CInt -> IO ()
+
+cuddSetNextReordering :: DDManager s u -> Int -> ST s ()
+cuddSetNextReordering = setIntegral c_cuddSetNextReordering
+
+foreign import ccall safe "Cudd_ReadMaxGrowthAlternate"
+	c_cuddReadMaxGrowthAlternate :: Ptr CDDManager -> IO CDouble
+
+cuddReadMaxGrowthAlternate :: DDManager s u -> ST s Double
+cuddReadMaxGrowthAlternate = readFloat c_cuddReadMaxGrowthAlternate
+
+foreign import ccall safe "Cudd_SetMaxGrowthAlternate"
+	c_cuddSetMaxGrowthAlternate :: Ptr CDDManager -> CDouble -> IO ()
+
+cuddSetMaxGrowthAlternate :: DDManager s u -> Double -> ST s ()
+cuddSetMaxGrowthAlternate = setFloat c_cuddSetMaxGrowthAlternate
+
+foreign import ccall safe "Cudd_ReadMaxGrowth"
+	c_cuddReadMaxGrowth :: Ptr CDDManager -> IO CDouble
+
+cuddReadMaxGrowth :: DDManager s u -> ST s Double
+cuddReadMaxGrowth = readFloat c_cuddReadMaxGrowth
+
+foreign import ccall safe "Cudd_SetMaxGrowth"
+	c_cuddSetMaxGrowth :: Ptr CDDManager -> CDouble -> IO ()
+
+cuddSetMaxGrowth :: DDManager s u -> Double -> ST s ()
+cuddSetMaxGrowth = setFloat c_cuddSetMaxGrowth
+
+foreign import ccall safe "Cudd_ReadReorderingCycle"
+	c_cuddReadReorderingCycle :: Ptr CDDManager -> IO (CInt)
+
+cuddReadReorderingCycle :: DDManager s u -> ST s Int
+cuddReadReorderingCycle = readIntegral c_cuddReadReorderingCycle
+
+foreign import ccall safe "Cudd_SetReorderingCycle"
+	c_cuddSetReorderingCycle :: Ptr CDDManager -> CInt -> IO ()
+
+cuddSetReorderingCycle :: DDManager s u -> Int -> ST s ()
+cuddSetReorderingCycle = setIntegral c_cuddSetReorderingCycle
+
+--Genetic algorithm
+foreign import ccall safe "Cudd_ReadPopulationSize"
+	c_cuddReadPopulationSize :: Ptr CDDManager -> IO (CInt)
+
+cuddReadPopulationSize :: DDManager s u -> ST s Int
+cuddReadPopulationSize = readIntegral c_cuddReadPopulationSize
+
+foreign import ccall safe "Cudd_SetPopulationSize"
+	c_cuddSetPopulationSize :: Ptr CDDManager -> CInt -> IO ()
+
+cuddSetPopulationSize :: DDManager s u -> Int -> ST s ()
+cuddSetPopulationSize = setIntegral c_cuddSetPopulationSize
+
+foreign import ccall safe "Cudd_ReadNumberXovers"
+	c_cuddReadNumberXovers :: Ptr CDDManager -> IO (CInt)
+
+cuddReadNumberXovers :: DDManager s u -> ST s Int
+cuddReadNumberXovers = readIntegral c_cuddReadNumberXovers
+
+foreign import ccall safe "Cudd_SetNumberXovers"
+	c_cuddSetNumberXovers :: Ptr CDDManager -> CInt -> IO ()
+
+cuddSetNumberXovers :: DDManager s u -> Int -> ST s ()
+cuddSetNumberXovers = setIntegral c_cuddSetNumberXovers
+
+reordGCHook :: HookTyp
+reordGCHook _ _ _ = do
+    performGC
+    return 1
+
+foreign import ccall "wrapper"
+    makeFunPtr :: HookTyp -> IO (FunPtr HookTyp)
+
+regReordGCHook :: DDManager s u -> ST s Int
+regReordGCHook m = do
+    hk <- unsafeIOToST $ makeFunPtr reordGCHook
+    cuddAddHook m hk CuddPreReorderingHook
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Adam Walker
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Adam Walker nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/c_sources/cuddwrap.c b/c_sources/cuddwrap.c
new file mode 100644
--- /dev/null
+++ b/c_sources/cuddwrap.c
@@ -0,0 +1,109 @@
+#include <stdio.h>
+#include <math.h>
+#include <assert.h>
+
+#include "util.h"
+#include "cudd.h"
+
+//Function wrappers around macros
+DdNode *wrappedRegular(DdNode *f){
+    assert(f);
+    return Cudd_Regular(f);
+}
+
+void wrappedCuddRef(DdNode *f){
+	assert(f);
+	Cudd_Ref(f);
+}
+
+int wrappedCuddIsComplement(DdNode *f){
+    return Cudd_IsComplement(f);
+}
+
+//Garbage collection hooks
+int preGCHook_sample(DdManager *dd, const char *str, void *data){
+	printf("Performing %s garbage collection...", str);
+	return 1;
+}
+
+int postGCHook_sample(DdManager *dd, const char *str, void *data){
+	printf("%s GC done\n", str);
+	return 1;
+}
+
+//Wrappers around enumeration of satisfying assignments and prime implicants
+int **allSat(DdManager *m, DdNode *n, int *nterms, int *nvars){
+    CUDD_VALUE_TYPE value;
+    DdGen *gen;
+    int *cube;
+    int size = Cudd_ReadSize(m);
+    int num = ceil(Cudd_CountPathsToNonZero(n));
+    int i=0;
+
+    *nterms = num;
+    *nvars = size;
+
+    int **result = malloc(sizeof(int *)*num);
+    assert(result);
+    Cudd_ForeachCube(m, n, gen, cube, value){
+        result[i] = malloc(sizeof(int *)*size);
+        assert(result[i]);
+        int j;
+        for(j=0; j<size; j++){
+            result[i][j] = cube[j];
+        }
+        i++;
+    }
+
+    return result;
+}
+
+int *oneSat(DdManager *m, DdNode *n, int *nvars){
+    CUDD_VALUE_TYPE value;
+    DdGen *gen;
+    int *cube;
+    int size = Cudd_ReadSize(m);
+    int j;
+
+    *nvars = size;
+
+    gen = Cudd_FirstCube(m, n, &cube, &value);
+    if (Cudd_IsGenEmpty(gen)) {
+        Cudd_GenFree (gen);
+        return NULL;
+    }
+    
+    int *result = malloc(sizeof(int) * size);
+    assert(result);
+    for(j=0; j<size; j++){
+        result[j] = cube[j];
+    }
+    Cudd_GenFree (gen);
+
+    return result;
+}
+
+int *onePrime(DdManager *m, DdNode *l, DdNode *u, int *nvars){
+    DdGen *gen;
+    int *cube;
+    int size = Cudd_ReadSize(m);
+    int j;
+
+    *nvars = size;
+
+    gen = Cudd_FirstPrime(m, l, u, &cube);
+    if (Cudd_IsGenEmpty(gen)) {
+        Cudd_GenFree (gen);
+        return NULL;
+    }
+    
+    int *result = malloc(sizeof(int) * size);
+    assert(result);
+    for(j=0; j<size; j++){
+        result[j] = cube[j];
+    }
+    Cudd_GenFree (gen);
+
+    return result;
+}
+
diff --git a/c_sources/stubs.c b/c_sources/stubs.c
new file mode 100644
--- /dev/null
+++ b/c_sources/stubs.c
@@ -0,0 +1,294 @@
+#include <stdio.h>
+#include <assert.h>
+#include "cudd.h"
+#include "dddmp.h"
+
+DdNode *Cudd_bddVarMap_s(DdManager *m, DdNode *x){
+    DdNode *r = Cudd_bddVarMap(m, x);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_ReadOne_s(DdManager *m){
+    DdNode *r = Cudd_ReadOne(m);
+    assert(r);
+    return r;
+}
+
+DdNode *Cudd_ReadLogicZero_s(DdManager *m){
+    DdNode *r = Cudd_ReadLogicZero(m);
+    assert(r);
+    return r;
+}
+
+DdNode *Cudd_ReadOne_withRef_s(DdManager *m){
+    DdNode *r = Cudd_ReadOne(m);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_ReadLogicZero_withRef_s(DdManager *m){
+    DdNode *r = Cudd_ReadLogicZero(m);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddIthVar_s(DdManager *m, int i){
+    DdNode *r = Cudd_bddIthVar(m, i);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddNewVarAtLevel_s(DdManager *m, int i){
+    DdNode *r = Cudd_bddNewVarAtLevel(m, i);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddAnd_s(DdManager *m, DdNode *x, DdNode *y){
+    DdNode *r = Cudd_bddAnd(m, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddOr_s(DdManager *m, DdNode *x, DdNode *y){
+    DdNode *r = Cudd_bddOr(m, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddNand_s(DdManager *m, DdNode *x, DdNode *y){
+    DdNode *r = Cudd_bddNand(m, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddNor_s(DdManager *m, DdNode *x, DdNode *y){
+    DdNode *r = Cudd_bddNor(m, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddXor_s(DdManager *m, DdNode *x, DdNode *y){
+    DdNode *r = Cudd_bddXor(m, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddXnor_s(DdManager *m, DdNode *x, DdNode *y){
+    DdNode *r = Cudd_bddXnor(m, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_Not_s(DdNode *x){
+    DdNode *r = Cudd_Not(x);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_NotNoRef_s(DdNode *x){
+    DdNode *r = Cudd_Not(x);
+    return r;
+}
+
+DdNode *Cudd_bddExistAbstract_s(DdManager *m, DdNode *x, DdNode *y){
+    DdNode *r = Cudd_bddExistAbstract(m, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddUnivAbstract_s(DdManager *m, DdNode *x, DdNode *y){
+    DdNode *r = Cudd_bddUnivAbstract(m, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddIte_s(DdManager *m, DdNode *x, DdNode *y, DdNode *z){
+    DdNode *r = Cudd_bddIte(m, x, y, z);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddSwapVariables_s(DdManager *m, DdNode *x, DdNode **y, DdNode **z, int i){
+    DdNode *r = Cudd_bddSwapVariables(m, x, y, z, i);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddPermute_s(DdManager *m, DdNode *x, int *p){
+    DdNode *r = Cudd_bddPermute(m, x, p);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_Xgty_s(DdManager *m, int i, DdNode **x, DdNode **y, DdNode **z){
+    DdNode *r = Cudd_Xgty(m, i, x, y, z);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_Xeqy_s(DdManager *m, int i, DdNode **x, DdNode **y){
+    DdNode *r = Cudd_Xeqy(m, i, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_Inequality_s(DdManager *m, int i, int j, DdNode **x, DdNode **y){
+    DdNode *r = Cudd_Inequality(m, i, j, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+    
+DdNode *Cudd_Disequality_s(DdManager *m, int i, int j, DdNode **x, DdNode **y){
+    DdNode *r = Cudd_Disequality(m, i, j, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddInterval_s(DdManager *m, int i, DdNode **x, int j, int k){
+    DdNode *r = Cudd_bddInterval(m, i, x, j, k);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_IndicesToCube_s(DdManager *m, int *i, int j){
+    DdNode *r = Cudd_IndicesToCube(m, i, j);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddLICompaction_s(DdManager *m, DdNode *x, DdNode *y){
+    DdNode *r = Cudd_bddLICompaction(m, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddMinimize_s(DdManager *m, DdNode *x, DdNode *y){
+    DdNode *r = Cudd_bddMinimize(m, x, y);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Dddmp_cuddBddLoad_s(DdManager *m, int i, char **s, int *j, int *k, int l, char *t, FILE *f){
+    DdNode *r = Dddmp_cuddBddLoad(m, i, s, j, k, l, t, f);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddPickOneMinterm_s(DdManager *m, DdNode *x, DdNode **y, int i){
+    DdNode *r = Cudd_bddPickOneMinterm(m, x, y, i);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddAndAbstract_s(DdManager *m, DdNode *x, DdNode *y, DdNode *z){
+    DdNode *r = Cudd_bddAndAbstract(m, x, y, z);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddXorExistAbstract_s(DdManager *m, DdNode *x, DdNode *y, DdNode *z){
+    DdNode *r = Cudd_bddXorExistAbstract(m, x, y, z);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddMakePrime_s(DdManager *m, DdNode *c, DdNode *f){
+    DdNode *r = Cudd_bddMakePrime(m, c, f);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddRestrict_s(DdManager *m, DdNode *f, DdNode *c){
+    DdNode *r = Cudd_bddRestrict(m, f, c);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddSqueeze_s(DdManager *m, DdNode *l, DdNode *u){
+    DdNode *r = Cudd_bddSqueeze(m, l, u);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddConstrain_s(DdManager *m, DdNode *f, DdNode *c){
+    DdNode *r = Cudd_bddConstrain(m, f, c);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_LargestCube_s(DdManager *m, DdNode *f, int *length){
+    DdNode *r = Cudd_LargestCube(m, f, length);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddComputeCube_s(DdManager *m, DdNode **vars, int *phase, int n){
+    DdNode *r = Cudd_bddComputeCube(m, vars, phase, n);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddCompose_s(DdManager *m, DdNode *f, DdNode *g, int v){
+    DdNode *r = Cudd_bddCompose(m, f, g, v);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_Support_s(DdManager *m, DdNode *f) {
+    DdNode *r = Cudd_Support(m, f);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddNewVar_s(DdManager *m){
+    DdNode *r = Cudd_bddNewVar(m);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
+DdNode *Cudd_bddVectorCompose_s(DdManager *m, DdNode *x, DdNode **xs){
+    DdNode *r = Cudd_bddVectorCompose(m, x, xs);
+    assert(r);
+    Cudd_Ref(r);
+    return r;
+}
+
diff --git a/cudd.cabal b/cudd.cabal
new file mode 100644
--- /dev/null
+++ b/cudd.cabal
@@ -0,0 +1,32 @@
+-- Initial cudd.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+name:                cudd
+version:             0.1.0.0
+synopsis:            Bindings to the CUDD binary decision diagrams library
+description:         Bindings to the CUDD binary decision diagrams library. 
+                     .
+                     <http://vlsi.colorado.edu/~fabio/CUDD/>
+license:             BSD3
+license-file:        LICENSE
+author:              Adam Walker
+maintainer:          adamwalker10@gmail.com
+copyright:           2014 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:  
+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