diff --git a/Cudd/C.hs b/Cudd/C.hs
new file mode 100644
index 0000000..4bd4921
--- /dev/null
+++ b/Cudd/C.hs
@@ -0,0 +1,343 @@
+{-# LANGUAGE ForeignFunctionInterface, EmptyDataDecls, CPP #-}
+
+module Cudd.C (
+    CDdManager,
+    CDdNode,
+    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
+    ) where
+
+import Foreign
+import Foreign.C.Types
+
+import Cudd.MTR
+
+data CDdManager
+data CDdNode
+
+foreign import ccall safe "cudd.h Cudd_ReadOne_s"
+	c_cuddReadOne :: Ptr CDdManager -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_ReadLogicZero_s"
+	c_cuddReadLogicZero :: Ptr CDdManager -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_ReadOne_withRef_s"
+	c_cuddReadOneWithRef :: Ptr CDdManager -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_ReadLogicZero_withRef_s"
+	c_cuddReadLogicZeroWithRef :: Ptr CDdManager -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddIthVar_s"
+	c_cuddBddIthVar :: Ptr CDdManager -> CInt -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddAnd_s"
+	c_cuddBddAnd :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddOr_s"
+	c_cuddBddOr :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddNand_s"
+	c_cuddBddNand :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddNor_s"
+	c_cuddBddNor :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddXor_s"
+	c_cuddBddXor :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddXnor_s"
+	c_cuddBddXnor :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_Not_s"
+	c_cuddNot :: Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_NotNoRef_s"
+	c_cuddNotNoRef :: Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddIte_s"
+    c_cuddBddIte :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddExistAbstract_s"
+	c_cuddBddExistAbstract :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddUnivAbstract_s"
+	c_cuddBddUnivAbstract :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_IterDerefBdd"
+	c_cuddIterDerefBdd :: Ptr CDdManager -> Ptr CDdNode -> IO ()
+
+foreign import ccall safe "cuddwrap.h wrappedCuddRef"
+	cuddRef :: Ptr CDdNode -> IO ()
+
+foreign import ccall safe "cudd.h Cudd_Init"
+	c_cuddInit :: CInt -> CInt -> CInt -> CInt -> CInt -> IO (Ptr CDdManager)
+
+foreign import ccall safe "cudd.h Cudd_ShuffleHeap"
+    c_cuddShuffleHeap :: Ptr CDdManager -> Ptr CInt -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_SetVarMap"
+    c_cuddSetVarMap :: Ptr CDdManager -> Ptr (Ptr CDdNode) -> Ptr (Ptr CDdNode) -> CInt -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_bddVarMap_s"
+    c_cuddBddVarMap :: Ptr CDdManager -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddLeq"
+    c_cuddBddLeq :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_bddSwapVariables_s"
+    c_cuddBddSwapVariables :: Ptr CDdManager -> Ptr CDdNode -> Ptr (Ptr CDdNode) -> Ptr (Ptr CDdNode) -> CInt -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_LargestCube_s"
+    c_cuddLargestCube :: Ptr CDdManager -> Ptr CDdNode -> Ptr CInt -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddMakePrime_s"
+    c_cuddBddMakePrime :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_Support_s"
+    c_cuddSupport :: Ptr CDdManager -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_SupportIndex"
+	c_cuddSupportIndex :: Ptr CDdManager -> Ptr CDdNode -> IO(Ptr CInt)
+
+foreign import ccall safe "cudd.h Cudd_SupportIndices"
+    c_cuddSupportIndices :: Ptr CDdManager -> Ptr CDdNode -> Ptr (Ptr CInt) -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_IndicesToCube_s"
+    c_cuddIndicesToCube :: Ptr CDdManager -> Ptr CInt -> CInt -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddComputeCube_s"
+    c_cuddBddComputeCube :: Ptr CDdManager -> Ptr (Ptr CDdNode) -> Ptr CInt -> CInt -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_BddToCubeArray"
+    c_cuddBddToCubeArray :: Ptr CDdManager -> Ptr CDdNode -> Ptr CInt -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_ReadSize"
+	c_cuddReadSize :: Ptr CDdManager -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_bddCompose_s"
+    c_cuddBddCompose :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> CInt -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddAndAbstract_s"
+    c_cuddBddAndAbstract :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddXorExistAbstract_s"
+    c_cuddBddXorExistAbstract :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddLeqUnless"
+    c_cuddBddLeqUnless :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> Ptr CDdNode -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_EquivDC"
+    c_cuddEquivDC :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> Ptr CDdNode -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_Xeqy_s"
+	c_cuddXeqy :: Ptr CDdManager -> CInt -> Ptr (Ptr CDdNode) -> Ptr (Ptr CDdNode) -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_DebugCheck"
+    c_cuddDebugCheck :: Ptr CDdManager -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_CheckKeys"
+    c_cuddCheckKeys :: Ptr CDdManager -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_bddPickOneMinterm_s"
+	c_cuddBddPickOneMinterm :: Ptr CDdManager -> Ptr CDdNode -> Ptr (Ptr CDdNode) -> CInt -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_CheckZeroRef"
+    c_cuddCheckZeroRef :: Ptr CDdManager -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_ReadInvPerm"
+    c_cuddReadInvPerm :: Ptr CDdManager -> CInt -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_ReadPerm"
+    c_cuddReadPerm :: Ptr CDdManager -> CInt -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_DagSize"
+    c_cuddDagSize :: Ptr CDdNode -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_ReadNodeCount"
+    c_cuddReadNodeCount :: Ptr CDdManager -> IO CLong
+
+foreign import ccall safe "cudd.h Cudd_ReadPeakNodeCount"
+    c_cuddReadPeakNodeCount :: Ptr CDdManager -> IO CLong
+
+foreign import ccall safe "cudd.h Cudd_ReadMaxCache"
+    c_cuddReadMaxCache :: Ptr CDdManager -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_ReadMaxCacheHard"
+    c_cuddReadMaxCacheHard :: Ptr CDdManager -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_SetMaxCacheHard"
+    c_cuddSetMaxCacheHard :: Ptr CDdManager -> CInt -> IO ()
+
+foreign import ccall safe "cudd.h Cudd_ReadCacheSlots"
+    c_cuddReadCacheSlots :: Ptr CDdManager -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_ReadCacheUsedSlots"
+    c_cuddReadCacheUsedSlots :: Ptr CDdManager -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_bddAndLimit"
+    c_cuddBddAndLimit :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> CUInt -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddNewVarAtLevel_s"
+    c_cuddBddNewVarAtLevel :: Ptr CDdManager -> CInt -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_ReadTree"
+    c_cuddReadTree :: Ptr CDdManager -> IO (Ptr CMtrNode)
+
+foreign import ccall safe "cudd.h Cudd_bddLICompaction_s"
+    c_cuddBddLICompaction :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddSqueeze_s" 
+    c_cuddBddSqueeze :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddMinimize_s"
+    c_cuddBddMinimize :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_Eval"
+    c_cuddEval :: Ptr CDdManager -> Ptr CDdNode -> Ptr CInt -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd,h Cudd_CountLeaves"
+    c_cuddCountLeaves :: Ptr CDdNode -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_CountMinterm"
+    c_cuddCountMinterm :: Ptr CDdManager -> Ptr CDdNode -> CInt -> IO CDouble
+
+foreign import ccall safe "cudd.h Cudd_CountPathsToNonZero"
+    c_cuddCountPathsToNonZero :: Ptr CDdNode -> IO CDouble
+
+foreign import ccall safe "cudd.h Cudd_CountPath"
+    c_cuddCountPath :: Ptr CDdNode -> IO CDouble
+
+foreign import ccall safe "cudd.h Cudd_bddConstrain_s"
+    c_cuddBddConstrain :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddRestrict_s"
+    c_cuddBddRestrict :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h wrappedRegular"
+    c_wrappedRegular :: Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddPermute_s"
+    c_cuddBddPermute :: Ptr CDdManager -> Ptr CDdNode -> Ptr CInt -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h 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.h Cudd_Inequality_s"
+	c_cuddInequality :: Ptr CDdManager -> CInt -> CInt -> Ptr (Ptr CDdNode) -> Ptr (Ptr CDdNode) -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_Disequality_s"
+	c_cuddDisequality :: Ptr CDdManager -> CInt -> CInt -> Ptr (Ptr CDdNode) -> Ptr (Ptr CDdNode) -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddInterval_s"
+    c_cuddBddInterval :: Ptr CDdManager -> CInt -> Ptr (Ptr CDdNode) -> CInt -> CInt -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_NodeReadIndex"
+    c_cuddNodeReadIndex :: Ptr CDdNode -> IO CInt
+
+foreign import ccall safe "cudd.h Cudd_bddTransfer"
+    c_cuddBddTransfer :: Ptr CDdManager -> Ptr CDdManager -> Ptr CDdNode -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h &Cudd_RecursiveDeref"
+	c_cuddRecursiveDerefPtr :: FunPtr (Ptr CDdManager -> Ptr CDdNode -> IO ())
+
+foreign import ccall safe "cudd.h &Cudd_DelayedDerefBdd"
+	c_cuddDelayedDerefBddPtr :: FunPtr (Ptr CDdManager -> Ptr CDdNode -> IO ())
+
+foreign import ccall safe "cudd.h &Cudd_IterDerefBdd"
+	c_cuddIterDerefBddPtr :: FunPtr (Ptr CDdManager -> Ptr CDdNode -> IO ())
+
+foreign import ccall safe "cudd.h Cudd_bddNewVar_s"
+    c_cuddBddNewVar :: Ptr CDdManager -> IO (Ptr CDdNode)
+
+foreign import ccall safe "cudd.h Cudd_bddVectorCompose_s"
+    c_cuddBddVectorCompose :: Ptr CDdManager -> Ptr CDdNode -> Ptr (Ptr CDdNode) -> IO (Ptr CDdNode) 
+
+foreign import ccall safe "cudd.h Cudd_Quit"
+    c_cuddQuit :: Ptr CDdManager -> IO ()
+
+foreign import ccall safe "cudd.h Cudd_PrintMinterm"
+    c_cuddPrintMinterm :: Ptr CDdManager -> Ptr CDdNode -> IO ()
+
+foreign import ccall safe "Cudd_CheckCube"
+    c_cuddCheckCube :: Ptr CDdManager -> Ptr CDdNode -> IO CInt
+
diff --git a/Cudd/Common.hs b/Cudd/Common.hs
new file mode 100644
index 0000000..d1639d5
--- /dev/null
+++ b/Cudd/Common.hs
@@ -0,0 +1,15 @@
+module Cudd.Common where
+
+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]
+
diff --git a/Cudd/Convert.hs b/Cudd/Convert.hs
new file mode 100644
index 0000000..eff09a9
--- /dev/null
+++ b/Cudd/Convert.hs
@@ -0,0 +1,25 @@
+module Cudd.Convert where
+
+import System.IO.Unsafe
+import Foreign.ForeignPtr
+import Foreign.ForeignPtr.Unsafe
+import Control.Monad.ST
+import Control.Monad.ST.Unsafe
+
+import Cudd.Internal
+import Cudd.C
+
+toDdNode :: DdManager -> DDNode s u -> DdNode
+toDdNode (DdManager m) (DDNode d) = DdNode $ unsafePerformIO $ do 
+    cuddRef d
+    newForeignPtrEnv deref m d
+
+toDdManager :: STDdManager s u -> DdManager
+toDdManager = DdManager . unSTDdManager
+
+toDDNode :: DdNode -> ST s (DDNode s u)
+toDDNode (DdNode fp) = unsafeIOToST $ do
+    let p = unsafeForeignPtrToPtr fp
+    cuddRef p
+    return $ DDNode p
+
diff --git a/Cudd/Cudd.hs b/Cudd/Cudd.hs
new file mode 100644
index 0000000..b1e3cfc
--- /dev/null
+++ b/Cudd/Cudd.hs
@@ -0,0 +1,449 @@
+{-# LANGUAGE ForeignFunctionInterface, CPP, FlexibleContexts, RankNTypes #-}
+
+module Cudd.Cudd (
+    DdManager(),
+    DdNode(),
+    cuddInit,
+    cuddInitOrder,
+    cuddReadOne,
+    cuddReadLogicZero,
+    cuddBddIthVar,
+    cuddBddAnd,
+    cuddBddOr,
+    cuddBddNand,
+    cuddBddNor,
+    cuddBddXor,
+    cuddBddXnor,
+    cuddNot,
+    cuddDumpDot,
+    cudd_cache_slots,
+    cudd_unique_slots,
+    cuddEval,
+    cuddPrintMinterm,
+    cuddAllSat,
+    cuddOneSat,
+    cuddOnePrime,
+    cuddSupportIndex,
+    cuddBddExistAbstract,
+    cuddBddUnivAbstract,
+    cuddBddIte,
+    cuddBddPermute,
+    cuddBddShift,
+    cuddBddSwapVariables,
+    cuddNodeReadIndex,
+    cuddDagSize,
+    cuddIndicesToCube,
+    getManagerST,
+    getSTManager,
+    cuddBddLICompaction,
+    cuddBddMinimize,
+    cuddReadSize,
+    cuddXeqy,
+    cuddXgty,
+    cuddBddInterval,
+    cuddDisequality,
+    cuddInequality,
+    ddNodeToInt,
+    cuddBddImp,
+    cuddBddPickOneMinterm,
+    cuddReadPerm,
+    cuddReadInvPerm,
+    cuddReadPerms,
+    cuddReadInvPerms,
+    cuddReadTree,
+    cuddCountLeaves,
+    cuddCountMinterm,
+    cuddCountPath,
+    cuddCountPathsToNonZero,
+    cuddPrintDebug,
+    cuddBddAndAbstract,
+    cuddBddXorExistAbstract,
+    cuddBddTransfer,
+    cuddBddMakePrime,
+    cuddBddConstrain,
+    cuddBddRestrict,
+    cuddBddSqueeze,
+    SatBit(..),
+    cuddLargestCube,
+    cuddBddLeq,
+    cuddDebugCheck,
+    cuddCheckKeys,
+    cuddPrintInfo
+    ) 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.ST
+import Control.Monad.ST.Unsafe
+import Control.Monad
+import Data.List
+import Data.Array hiding (indices)
+import Control.Exception
+
+import Cudd.ForeignHelpers
+import Cudd.Internal
+import Cudd.MTR
+import Cudd.C
+import Cudd.Common
+
+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
+
+getManagerST :: STDdManager s u -> DdManager
+getManagerST (STDdManager m) = DdManager m
+
+getSTManager :: DdManager -> STDdManager s u
+getSTManager (DdManager m) = STDdManager m
+
+cuddReadOne :: DdManager -> DdNode
+cuddReadOne (DdManager d) = DdNode $ unsafePerformIO $ do
+	node <- c_cuddReadOneWithRef d
+	newForeignPtrEnv deref d node
+
+cuddReadLogicZero :: DdManager -> DdNode
+cuddReadLogicZero (DdManager d) = DdNode $ unsafePerformIO $ do
+	node <- c_cuddReadLogicZeroWithRef d
+	newForeignPtrEnv deref d node
+
+cuddBddIthVar :: DdManager -> Int -> DdNode
+cuddBddIthVar (DdManager d) i = DdNode $ unsafePerformIO $ do
+	node <- c_cuddBddIthVar d (fromIntegral i)
+	newForeignPtr_ 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
+
+cuddBddAnd :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddAnd = cuddArg2 c_cuddBddAnd
+
+cuddBddOr :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddOr = cuddArg2 c_cuddBddOr
+
+cuddBddNand :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddNand = cuddArg2 c_cuddBddNand
+
+cuddBddNor :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddNor = cuddArg2 c_cuddBddNor
+
+cuddBddXor :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddXor = cuddArg2 c_cuddBddXor
+
+cuddBddXnor :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddXnor = cuddArg2 c_cuddBddXnor
+
+cuddNot :: DdManager -> DdNode -> DdNode
+cuddNot = cuddArg1 (const c_cuddNot)
+
+foreign import ccall safe "cuddwrap.h wrappedCuddDumpDot"
+	c_cuddDumpDot :: Ptr CDdManager -> Ptr CDdNode -> CString -> IO ()
+
+cuddDumpDot :: DdManager -> DdNode -> String -> IO ()
+cuddDumpDot (DdManager m) (DdNode n) s  = 
+	withForeignPtr n $ \np -> 
+		withCAString s $ \str -> 
+			c_cuddDumpDot m np str
+
+foreign import ccall safe "cuddwrap.h wrappedCuddIsComplement"
+    c_cuddIsComplement :: Ptr CDdNode -> CInt
+
+cuddEval :: DdManager -> DdNode -> [Int] -> Bool
+cuddEval (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
+
+cuddPrintMinterm :: DdManager -> DdNode -> IO ()
+cuddPrintMinterm (DdManager m) (DdNode n) = 
+    withForeignPtr n $ c_cuddPrintMinterm m 
+
+foreign import ccall safe "cuddwrap.h allSat"
+    c_allSat :: Ptr CDdManager -> Ptr CDdNode -> Ptr CInt -> Ptr CInt -> IO (Ptr (Ptr CInt))
+
+foreign import ccall safe "cuddwrap.h oneSat"
+    c_oneSat :: Ptr CDdManager -> Ptr CDdNode -> Ptr CInt -> IO (Ptr CInt)
+
+cuddAllSat :: DdManager -> DdNode -> [[SatBit]]
+cuddAllSat (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
+
+cuddOneSat :: DdManager -> DdNode -> Maybe [SatBit]
+cuddOneSat (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 "cuddwrap.h onePrime"
+    c_onePrime :: Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> Ptr CInt -> IO (Ptr CInt)
+
+cuddOnePrime :: DdManager -> DdNode -> DdNode -> Maybe [Int]
+cuddOnePrime (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
+
+cuddReadSize :: DdManager -> Int
+cuddReadSize (DdManager m) = fromIntegral $ unsafePerformIO $ c_cuddReadSize m
+
+cuddSupportIndex :: DdManager -> DdNode -> [Bool]
+cuddSupportIndex (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
+
+cuddBddExistAbstract :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddExistAbstract = cuddArg2 c_cuddBddExistAbstract
+
+cuddBddUnivAbstract :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddUnivAbstract = cuddArg2 c_cuddBddUnivAbstract
+
+cuddBddIte :: DdManager -> DdNode -> DdNode -> DdNode -> DdNode
+cuddBddIte = cuddArg3 c_cuddBddIte
+
+cuddBddSwapVariables :: DdManager -> DdNode -> [DdNode] -> [DdNode] -> DdNode
+cuddBddSwapVariables (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
+
+cuddBddPermute :: DdManager -> DdNode -> [Int] -> DdNode 
+cuddBddPermute (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
+
+makePermutArray :: Int -> [Int] -> [Int] -> [Int]
+makePermutArray size x y = elems $ accumArray (flip const) 0 (0, size-1) ascList
+    where
+    ascList = [(i, i) | i <- [0..size-1]] ++ zip x y 
+
+cuddBddShift :: DdManager -> DdNode -> [Int] -> [Int] -> DdNode
+cuddBddShift (DdManager m) (DdNode d) from to = DdNode $ unsafePerformIO $
+    withForeignPtr d $ \dp -> do
+    dp <- evaluate dp
+    size <- c_cuddReadSize m 
+    let perm = makePermutArray (fromIntegral size) from to
+    withArray (map fromIntegral perm) $ \pp -> do
+        node <- c_cuddBddPermute m dp pp
+        newForeignPtrEnv deref m node
+
+cuddXgty :: DdManager -> [DdNode] -> [DdNode] -> DdNode
+cuddXgty (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
+
+cuddXeqy :: DdManager -> [DdNode] -> [DdNode] -> DdNode
+cuddXeqy (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
+
+cuddInequality :: DdManager -> Int -> Int -> [DdNode] -> [DdNode] -> DdNode
+cuddInequality (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
+
+cuddDisequality :: DdManager -> Int -> Int -> [DdNode] -> [DdNode] -> DdNode
+cuddDisequality (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
+
+cuddBddInterval :: DdManager -> [DdNode] -> Int -> Int -> DdNode
+cuddBddInterval (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
+
+cuddNodeReadIndex :: DdNode -> Int
+cuddNodeReadIndex (DdNode d) = fromIntegral $ unsafePerformIO $ withForeignPtr d c_cuddNodeReadIndex 
+
+cuddDagSize (DdNode d) = fromIntegral $ unsafePerformIO $ withForeignPtr d c_cuddDagSize 
+
+cuddIndicesToCube :: DdManager -> [Int] -> DdNode
+cuddIndicesToCube (DdManager m) indices = DdNode $ unsafePerformIO $ 
+    withArrayLen (map fromIntegral indices) $ \size ip -> do
+    node <- c_cuddIndicesToCube m ip (fromIntegral size)
+    newForeignPtrEnv deref m node
+
+cuddBddLICompaction :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddLICompaction = cuddArg2 c_cuddBddLICompaction
+
+cuddBddMinimize :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddMinimize = cuddArg2 c_cuddBddMinimize
+
+--Bdd implication
+cuddBddImp :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddImp m l r = cuddBddOr m (cuddNot m l) r
+
+cuddBddPickOneMinterm :: DdManager -> DdNode -> [DdNode] -> Maybe DdNode
+cuddBddPickOneMinterm (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
+
+foreign import ccall safe "cudd.h Cudd_PrintInfo"
+       c_cuddPrintInfo :: Ptr CDdManager -> Ptr CFile -> IO CInt
+                
+cuddPrintInfo :: DdManager -> Ptr CFile -> IO Int
+cuddPrintInfo (DdManager m) cf = liftM fromIntegral $ c_cuddPrintInfo m cf
+
+cuddReadPerm :: DdManager -> Int -> Int
+cuddReadPerm (DdManager m) i = fromIntegral $ unsafePerformIO $ c_cuddReadPerm m (fromIntegral i)
+
+cuddReadInvPerm :: DdManager -> Int -> Int
+cuddReadInvPerm (DdManager m) i = fromIntegral $ unsafePerformIO $ c_cuddReadInvPerm m (fromIntegral i)
+
+cuddReadPerms :: DdManager -> [Int]
+cuddReadPerms m = map (cuddReadPerm m) [0..(cuddReadSize m - 1)]
+
+cuddReadInvPerms :: DdManager -> [Int]
+cuddReadInvPerms m = map (cuddReadInvPerm m) [0..(cuddReadSize m -1)]
+
+cuddReadTree :: DdManager -> IO (Ptr CMtrNode) 
+cuddReadTree (DdManager m) = c_cuddReadTree m
+
+cuddCountLeaves :: DdNode -> Int
+cuddCountLeaves (DdNode d) = fromIntegral $ unsafePerformIO $ 
+    withForeignPtr d $ \dp -> 
+    c_cuddCountLeaves dp
+
+cuddCountMinterm :: DdManager -> DdNode -> Int -> Double
+cuddCountMinterm (DdManager m) (DdNode d) n = realToFrac $ unsafePerformIO $
+    withForeignPtr d $ \dp -> 
+    c_cuddCountMinterm m dp (fromIntegral n) 
+
+cuddCountPathsToNonZero :: DdNode -> Double
+cuddCountPathsToNonZero (DdNode d) = realToFrac $ unsafePerformIO $
+    withForeignPtr d $ \dp ->
+    c_cuddCountPathsToNonZero dp
+
+cuddCountPath :: DdNode -> Double
+cuddCountPath (DdNode d) = realToFrac $ unsafePerformIO $
+    withForeignPtr d $ \dp -> 
+    c_cuddCountPath dp
+
+foreign import ccall safe "cudd.h Cudd_PrintDebug"
+    c_cuddPrintDebug :: Ptr CDdManager -> Ptr CDdNode -> CInt -> CInt -> IO CInt
+
+cuddPrintDebug :: DdManager -> DdNode -> Int -> Int -> IO Int
+cuddPrintDebug (DdManager m) (DdNode d) n pr = liftM fromIntegral $ 
+    withForeignPtr d $ \dp -> 
+    c_cuddPrintDebug m dp (fromIntegral n) (fromIntegral pr)
+
+cuddBddAndAbstract :: DdManager -> DdNode -> DdNode -> DdNode -> DdNode  
+cuddBddAndAbstract = cuddArg3 c_cuddBddAndAbstract
+
+cuddBddXorExistAbstract :: DdManager -> DdNode -> DdNode -> DdNode -> DdNode  
+cuddBddXorExistAbstract = cuddArg3 c_cuddBddXorExistAbstract
+
+cuddBddTransfer :: DdManager -> DdManager -> DdNode -> DdNode
+cuddBddTransfer (DdManager m1) (DdManager m2) (DdNode x) = DdNode $ unsafePerformIO $ 
+    withForeignPtr x $ \xp -> do
+        node <- c_cuddBddTransfer m1 m2 xp
+        newForeignPtrEnv deref m2 node
+
+cuddBddMakePrime :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddMakePrime = cuddArg2 c_cuddBddMakePrime
+
+cuddBddConstrain :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddConstrain = cuddArg2 c_cuddBddConstrain
+
+cuddBddRestrict :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddRestrict = cuddArg2 c_cuddBddRestrict
+
+cuddBddSqueeze :: DdManager -> DdNode -> DdNode -> DdNode
+cuddBddSqueeze = cuddArg2 c_cuddBddSqueeze
+
+cuddLargestCube :: DdManager -> DdNode -> (Int, DdNode)
+cuddLargestCube (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)
+     
+cuddBddLeq :: DdManager -> DdNode -> DdNode -> Bool
+cuddBddLeq (DdManager m) (DdNode l) (DdNode r) = (==1) $ unsafePerformIO $ 
+    withForeignPtr l $ \lp -> 
+    withForeignPtr r $ \rp ->
+    c_cuddBddLeq m lp rp
+
+cuddCheckKeys :: DdManager -> ST s Int
+cuddCheckKeys (DdManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddCheckKeys m
+
+cuddDebugCheck :: DdManager -> ST s Int
+cuddDebugCheck (DdManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddDebugCheck m
+
+ddNodeToInt :: Integral i => DdNode -> i
+ddNodeToInt = fromIntegral . ptrToIntPtr . unsafeForeignPtrToPtr . unDdNode 
+
diff --git a/Cudd/File.chs b/Cudd/File.chs
new file mode 100644
index 0000000..71b3bf1
--- /dev/null
+++ b/Cudd/File.chs
@@ -0,0 +1,66 @@
+{-# LANGUAGE ForeignFunctionInterface, CPP, FlexibleContexts, RankNTypes #-}
+
+module Cudd.File 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.Error
+
+import Cudd.Internal
+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.h 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.h 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
index 0000000..99d9176
--- /dev/null
+++ b/Cudd/ForeignHelpers.hs
@@ -0,0 +1,18 @@
+module Cudd.ForeignHelpers (
+    withForeignArray,
+    withForeignArrayPtr,
+    withForeignArrayPtrLen
+    ) where
+
+import Foreign
+
+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)
+
+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
diff --git a/Cudd/GC.hs b/Cudd/GC.hs
new file mode 100644
index 0000000..12c8657
--- /dev/null
+++ b/Cudd/GC.hs
@@ -0,0 +1,58 @@
+{-#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 Foreign.Marshal.Array
+import Foreign.Marshal.Utils
+import Control.Monad
+import Control.Monad.ST
+import Control.Monad.ST.Unsafe
+
+import Cudd.Internal
+import Cudd.Hook
+import Cudd.C
+
+foreign import ccall safe "cudd.h Cudd_EnableGarbageCollection"
+	c_cuddEnableGarbageCollection :: Ptr CDdManager -> IO ()
+
+cuddEnableGarbageCollection :: STDdManager s u -> ST s ()
+cuddEnableGarbageCollection (STDdManager m) = unsafeIOToST $ c_cuddEnableGarbageCollection m
+
+foreign import ccall safe "cudd.h Cudd_DisableGarbageCollection"
+	c_cuddDisableGarbageCollection :: Ptr CDdManager -> IO ()
+
+cuddDisableGarbageCollection :: STDdManager s u -> ST s ()
+cuddDisableGarbageCollection (STDdManager m) = unsafeIOToST $ c_cuddDisableGarbageCollection m
+
+foreign import ccall safe "cudd.h Cudd_GarbageCollectionEnabled"
+	c_cuddGarbageCollectionEnabled :: Ptr CDdManager -> IO CInt
+
+cuddGarbageCollectionEnabled :: STDdManager s u -> ST s Int
+cuddGarbageCollectionEnabled (STDdManager m) = unsafeIOToST $ liftM fromIntegral $ c_cuddGarbageCollectionEnabled m
+
+foreign import ccall safe "cuddwrap.h &preGCHook_sample"
+	c_preGCHook_sample :: HookFP
+
+foreign import ccall safe "cuddwrap.h &postGCHook_sample"
+	c_postGCHook_sample :: HookFP
+
+regPreGCHook :: STDdManager s u -> HookFP -> ST s Int
+regPreGCHook m func = cuddAddHook m func CuddPreGcHook
+
+regPostGCHook :: STDdManager 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
index 0000000..b599d51
--- /dev/null
+++ b/Cudd/Hook.chs
@@ -0,0 +1,44 @@
+{-#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 Foreign.Marshal.Array
+import Foreign.Marshal.Utils
+import Control.Monad
+import Control.Monad.ST
+import Control.Monad.ST.Unsafe
+
+import Cudd.Internal
+import Cudd.C
+
+#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.h Cudd_AddHook"
+	c_cuddAddHook :: Ptr CDdManager -> HookFP -> CInt -> IO (CInt)
+
+cuddAddHook :: STDdManager s u -> HookFP -> CuddHookType -> ST s Int
+cuddAddHook (STDdManager m) fp typ = unsafeIOToST $ liftM fromIntegral $ c_cuddAddHook m fp (fromIntegral $ fromEnum typ)
+	
+foreign import ccall safe "cudd.h Cudd_RemoveHook"
+	c_cuddRemoveHook :: Ptr CDdManager -> HookFP -> CInt -> IO (CInt)
+
+cuddRemoveHook :: STDdManager s u -> HookFP -> CuddHookType -> ST s Int
+cuddRemoveHook (STDdManager 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
index 0000000..88a77f5
--- /dev/null
+++ b/Cudd/Imperative.hs
@@ -0,0 +1,351 @@
+{-# LANGUAGE RankNTypes #-}
+
+module Cudd.Imperative (
+    cuddInit,
+    cuddInitDefaults,
+    withManager, 
+    withManagerDefaults,
+    withManagerIO,
+    withManagerIODefaults,
+    shuffleHeap,
+    bzero,
+    bone,
+    ithVar,
+    band,
+    bor,
+    bnand,
+    bnor,
+    bxor,
+    bxnor,
+    bnot,
+    bite,
+    bexists,
+    bforall,
+    deref,
+    setVarMap,
+    varMap,
+    DDNode,
+    STDdManager,
+    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,
+    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.Internal hiding (deref)
+import Cudd.MTR
+import Cudd.Common
+
+cuddInit :: Int -> Int -> Int -> Int -> Int -> ST s (STDdManager s u)
+cuddInit numVars numVarsZ numSlots cacheSize maxMemory = unsafeIOToST $ do
+    cm <- c_cuddInit (fromIntegral numVars) (fromIntegral numVarsZ) (fromIntegral numSlots) (fromIntegral cacheSize) (fromIntegral maxMemory)
+    return $ STDdManager cm
+
+cuddInitDefaults :: ST s (STDdManager s u)
+cuddInitDefaults = cuddInit 0 0 cudd_unique_slots cudd_cache_slots 0
+
+withManager :: Int -> Int -> Int -> Int -> Int -> (forall u. STDdManager 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. STDdManager 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. STDdManager 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. STDdManager RealWorld u -> m a) -> m a
+withManagerIODefaults f = do
+    res <- liftIO $ stToIO cuddInitDefaults
+    f res
+
+shuffleHeap :: STDdManager s u -> [Int] -> ST s ()
+shuffleHeap (STDdManager 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)) -> STDdManager s u -> ST s (DDNode s u)
+arg0 f (STDdManager m) = liftM DDNode $ unsafeIOToST $ f m
+
+arg1 :: (Ptr CDdManager -> Ptr CDdNode -> IO (Ptr CDdNode)) -> STDdManager s u -> DDNode s u -> ST s (DDNode s u)
+arg1 f (STDdManager m) (DDNode x) = liftM DDNode $ unsafeIOToST $ f m x
+
+arg2 :: (Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)) -> STDdManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)
+arg2 f (STDdManager m) (DDNode x) (DDNode y) = liftM DDNode $ unsafeIOToST $ f m x y
+    
+arg3 :: (Ptr CDdManager -> Ptr CDdNode -> Ptr CDdNode -> Ptr CDdNode -> IO (Ptr CDdNode)) -> STDdManager s u -> DDNode s u -> DDNode s u -> DDNode s u  -> ST s (DDNode s u)
+arg3 f (STDdManager m) (DDNode x) (DDNode y) (DDNode z) = liftM DDNode $ unsafeIOToST $ f m x y z
+
+bzero (STDdManager m) = DDNode $ unsafePerformIO $ c_cuddReadLogicZero m
+bone  (STDdManager 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 (STDdManager m) i = liftM DDNode $ unsafeIOToST $ c_cuddBddIthVar m (fromIntegral i)
+
+deref :: STDdManager s u -> DDNode s u -> ST s ()
+deref (STDdManager m) (DDNode x) = unsafeIOToST $ c_cuddIterDerefBdd m x
+
+setVarMap :: STDdManager s u -> [DDNode s u] -> [DDNode s u] -> ST s ()
+setVarMap (STDdManager 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 :: STDdManager s u -> DDNode s u -> ST s (DDNode s u)
+varMap (STDdManager m) (DDNode x) = liftM DDNode $ unsafeIOToST $ c_cuddBddVarMap m x
+
+leq :: STDdManager s u -> DDNode s u -> DDNode s u -> ST s Bool
+leq (STDdManager m) (DDNode x) (DDNode y) = liftM (==1) $ unsafeIOToST $ c_cuddBddLeq m x y
+
+swapVariables :: STDdManager s u -> [DDNode s u] -> [DDNode s u] -> DDNode s u -> ST s (DDNode s u)
+swapVariables (STDdManager 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 :: STDdManager s u -> DDNode s u -> ST s (DDNode s u, Int)
+largestCube (STDdManager m) (DDNode x) = unsafeIOToST $ 
+    alloca $ \lp -> do
+    res <- c_cuddLargestCube m x lp 
+    l <- peek lp
+    return (DDNode res, fromIntegral l)
+
+makePrime :: STDdManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)
+makePrime = arg2 c_cuddBddMakePrime
+
+support :: STDdManager s u -> DDNode s u -> ST s (DDNode s u)
+support = arg1 c_cuddSupport
+
+supportIndices :: STDdManager s u -> DDNode s u -> ST s [Int]
+supportIndices (STDdManager 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 :: STDdManager s u -> [Int] -> ST s (DDNode s u)
+indicesToCube (STDdManager m) indices = unsafeIOToST $
+    withArrayLen (map fromIntegral indices) $ \sz pt -> do
+    res <- c_cuddIndicesToCube m pt (fromIntegral sz)
+    return $ DDNode res
+
+computeCube :: STDdManager s u -> [DDNode s u] -> [Bool] -> ST s (DDNode s u)
+computeCube (STDdManager 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 :: STDdManager s u -> [DDNode s u] -> ST s (DDNode s u)
+nodesToCube (STDdManager m) nodes = unsafeIOToST $
+    withArrayLen (map unDDNode nodes) $ \sz pt -> do
+    res <- c_cuddBddComputeCube m pt nullPtr (fromIntegral sz)
+    return $ DDNode res
+
+readSize :: STDdManager s u -> ST s Int
+readSize (STDdManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadSize m
+
+bddToCubeArray :: STDdManager s u -> DDNode s u -> ST s [SatBit]
+bddToCubeArray ma@(STDdManager 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 :: STDdManager s u -> DDNode s u -> DDNode s u -> Int -> ST s (DDNode s u)
+compose (STDdManager 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) -> STDdManager s u -> DDNode s u -> DDNode s u -> DDNode s u  -> ST s Bool
+arg3Bool f (STDdManager m) (DDNode x) (DDNode y) (DDNode z) = liftM (==1) $ unsafeIOToST $ f m x y z
+
+leqUnless, equivDC :: STDdManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s Bool
+leqUnless = arg3Bool c_cuddBddLeqUnless
+equivDC   = arg3Bool c_cuddEquivDC
+
+xeqy :: STDdManager s u -> [DDNode s u] -> [DDNode s u] -> ST s (DDNode s u)
+xeqy (STDdManager 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 :: STDdManager s u -> ST s Int
+debugCheck (STDdManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddDebugCheck m
+
+checkKeys :: STDdManager s u -> ST s Int
+checkKeys (STDdManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddCheckKeys m
+
+pickOneMinterm :: STDdManager s u -> DDNode s u -> [DDNode s u] -> ST s (DDNode s u)
+pickOneMinterm (STDdManager m) (DDNode d) vars = unsafeIOToST $ 
+    withArrayLen (map unDDNode vars) $ \vl vp -> do
+        res <- c_cuddBddPickOneMinterm m d vp (fromIntegral vl)
+        return $ DDNode res
+
+checkZeroRef :: STDdManager s u -> ST s Int
+checkZeroRef (STDdManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddCheckZeroRef m
+
+readInvPerm :: STDdManager s u -> Int -> ST s Int
+readInvPerm (STDdManager m) offs = liftM fromIntegral $ unsafeIOToST $ c_cuddReadInvPerm m (fromIntegral offs)
+
+readPerm :: STDdManager s u -> Int -> ST s Int
+readPerm (STDdManager 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 :: STDdManager s u -> ST s Integer
+readNodeCount (STDdManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadNodeCount m
+
+readPeakNodeCount :: STDdManager s u -> ST s Integer
+readPeakNodeCount (STDdManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadPeakNodeCount m
+
+regular :: DDNode s u -> DDNode s u
+regular (DDNode x) = DDNode $ unsafePerformIO $ c_wrappedRegular x
+
+readMaxCache :: STDdManager s u -> ST s Int
+readMaxCache (STDdManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadMaxCache m
+
+readMaxCacheHard :: STDdManager s u -> ST s Int
+readMaxCacheHard (STDdManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadMaxCacheHard m
+
+setMaxCacheHard :: STDdManager s u -> Int -> ST s ()
+setMaxCacheHard (STDdManager m) x = unsafeIOToST $ c_cuddSetMaxCacheHard m (fromIntegral x)
+
+readCacheSlots :: STDdManager s u -> ST s Int
+readCacheSlots (STDdManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadCacheSlots m
+
+readCacheUsedSlots :: STDdManager s u -> ST s Int
+readCacheUsedSlots (STDdManager m) = liftM fromIntegral $ unsafeIOToST $ c_cuddReadCacheUsedSlots m
+
+andLimit :: STDdManager s u -> DDNode s u -> DDNode s u -> Int -> ST s (Maybe (DDNode s u))
+andLimit (STDdManager 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 :: STDdManager s u -> ST s (MtrNode s)
+readTree (STDdManager m) = liftM MtrNode $ unsafeIOToST $ c_cuddReadTree m
+
+newVarAtLevel :: STDdManager s u -> Int -> ST s (DDNode s u)
+newVarAtLevel (STDdManager m) level = liftM DDNode $ unsafeIOToST $ c_cuddBddNewVarAtLevel m (fromIntegral level)
+
+liCompaction = arg2 c_cuddBddLICompaction
+squeeze      = arg2 c_cuddBddSqueeze
+minimize     = arg2 c_cuddBddMinimize
+
+newVar :: STDdManager s u -> ST s (DDNode s u)
+newVar (STDdManager m) = liftM DDNode $ unsafeIOToST $ c_cuddBddNewVar m
+
+vectorCompose :: STDdManager s u -> DDNode s u -> [DDNode s u] -> ST s (DDNode s u)
+vectorCompose (STDdManager 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 :: STDdManager s u -> ST s ()
+quit (STDdManager m) = unsafeIOToST $ c_cuddQuit m
+
+readIndex :: DDNode s u -> ST s Int
+readIndex (DDNode x) = liftM fromIntegral $ unsafeIOToST $ c_cuddNodeReadIndex x
+
+printMinterm :: STDdManager s u -> DDNode s u -> ST s ()
+printMinterm (STDdManager m) (DDNode x) = unsafeIOToST $ c_cuddPrintMinterm m x
+
+checkCube :: STDdManager s u -> DDNode s u -> ST s Bool
+checkCube (STDdManager m) (DDNode x) = liftM (==1) $ unsafeIOToST $ c_cuddCheckCube m x
+
diff --git a/Cudd/Internal.hsc b/Cudd/Internal.hsc
new file mode 100644
index 0000000..4f120f6
--- /dev/null
+++ b/Cudd/Internal.hsc
@@ -0,0 +1,35 @@
+{-# LANGUAGE ForeignFunctionInterface, EmptyDataDecls, CPP #-}
+module Cudd.Internal (
+    DdManager(..), 
+    STDdManager(..), 
+    DdNode(..), 
+    DDNode(..),
+    deref,
+    cudd_unique_slots,
+    cudd_cache_slots
+    ) where
+
+import Foreign.Ptr
+import Foreign.ForeignPtr
+
+import Cudd.C
+
+#include <stdio.h>
+#include "cudd.h"
+
+cudd_unique_slots :: Int
+cudd_unique_slots = #const CUDD_UNIQUE_SLOTS
+
+cudd_cache_slots :: Int
+cudd_cache_slots = #const CUDD_CACHE_SLOTS
+
+newtype DdManager = DdManager (Ptr CDdManager)
+
+newtype STDdManager s u = STDdManager {unSTDdManager :: Ptr CDdManager}
+
+newtype DdNode = DdNode {unDdNode :: ForeignPtr CDdNode} deriving (Ord, Eq, Show)
+
+newtype DDNode s u = DDNode {unDDNode :: Ptr CDdNode} deriving (Ord, Eq, Show)
+
+deref = c_cuddIterDerefBddPtr
+
diff --git a/Cudd/MTR.chs b/Cudd/MTR.chs
new file mode 100644
index 0000000..cedf40a
--- /dev/null
+++ b/Cudd/MTR.chs
@@ -0,0 +1,108 @@
+{-# LANGUAGE ForeignFunctionInterface, EmptyDataDecls, CPP #-}
+
+module Cudd.MTR 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.h Mtr_AllocNode"
+    c_mtrAllocNode :: IO (Ptr CMtrNode)
+
+mtrAllocNode :: ST s (MtrNode s) 
+mtrAllocNode = liftM MtrNode $ unsafeIOToST c_mtrAllocNode
+
+foreign import ccall unsafe "mtr.h 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.h 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.h Mtr_DeallocNode"
+    c_mtrDeallocNode :: Ptr CMtrNode -> IO ()
+
+mtrDeallocNode :: MtrNode s -> ST s ()
+mtrDeallocNode (MtrNode p) = unsafeIOToST $ c_mtrDeallocNode p
+
+foreign import ccall unsafe "mtr.h 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.h 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.h 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.h 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.h Mtr_PrintTree"
+    c_mtrPrintTree :: Ptr CMtrNode -> IO ()
+
+mtrPrintTree :: MtrNode s -> ST s ()
+mtrPrintTree (MtrNode c) = unsafeIOToST $ c_mtrPrintTree c
+
+foreign import ccall unsafe "mtr.h 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.h 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.h 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.h 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
index 0000000..b49e124
--- /dev/null
+++ b/Cudd/Reorder.chs
@@ -0,0 +1,287 @@
+{-#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 Foreign.Marshal.Array
+import Foreign.Marshal.Utils
+import Control.Monad
+import Control.Monad.ST
+import Control.Monad.ST.Unsafe
+
+import Cudd.Internal
+import Cudd.C
+import Cudd.Hook
+
+#include <stdio.h>
+#include <cudd.h>
+
+readIntegral :: (Integral i, Num j) => (Ptr CDdManager -> IO i) -> STDdManager s u -> ST s j
+readIntegral f (STDdManager m) = unsafeIOToST $ liftM fromIntegral $ f m
+
+setIntegral :: (Integral i, Num j) => (Ptr CDdManager -> j -> IO ()) -> STDdManager s u -> i -> ST s ()
+setIntegral f (STDdManager m) v = unsafeIOToST $ f m (fromIntegral v)
+
+readFloat :: (Real r, Fractional f) => (Ptr CDdManager -> IO r) -> STDdManager s u -> ST s f
+readFloat f (STDdManager m) = unsafeIOToST $ liftM realToFrac $ f m 
+
+setFloat :: (Real r, Fractional f) => (Ptr CDdManager -> f -> IO ()) -> STDdManager s u -> r -> ST s ()
+setFloat f (STDdManager 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.h Cudd_ReorderingStatus"
+	c_cuddReorderingStatus :: Ptr CDdManager -> Ptr CInt -> IO (CInt)
+
+cuddReorderingStatus :: STDdManager s u -> ST s (Int, CuddReorderingType)
+cuddReorderingStatus (STDdManager 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.h Cudd_AutodynEnable"
+	c_cuddAutodynEnable :: Ptr CDdManager -> CInt -> IO ()
+
+cuddAutodynEnable :: STDdManager s u -> CuddReorderingType -> ST s ()
+cuddAutodynEnable (STDdManager m) t = unsafeIOToST $ c_cuddAutodynEnable m (fromIntegral $ fromEnum t)
+
+foreign import ccall safe "cudd.h Cudd_AutodynDisable"
+	c_cuddAutodynDisable :: Ptr CDdManager -> IO ()
+
+cuddAutodynDisable :: STDdManager s u -> ST s ()
+cuddAutodynDisable (STDdManager m) = unsafeIOToST $ c_cuddAutodynDisable m
+
+--Reorder right now
+foreign import ccall safe "cudd.h Cudd_ReduceHeap"
+	c_cuddReduceHeap :: Ptr CDdManager -> CInt -> CInt -> IO (CInt)
+
+cuddReduceHeap :: STDdManager s u -> CuddReorderingType -> Int -> ST s Int
+cuddReduceHeap (STDdManager m) typ minsize = unsafeIOToST $ liftM fromIntegral $ c_cuddReduceHeap m (fromIntegral $ fromEnum typ) (fromIntegral minsize)
+
+--Grouping
+foreign import ccall safe "cudd.h Cudd_MakeTreeNode"
+	c_cuddMakeTreeNode :: Ptr CDdManager -> CUInt -> CUInt -> CUInt -> IO (Ptr ())
+
+cuddMakeTreeNode :: STDdManager s u -> Int -> Int -> Int -> ST s (Ptr ())
+cuddMakeTreeNode (STDdManager 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.h Cudd_ReadReorderingTime"
+	c_cuddReadReorderingTime :: Ptr CDdManager -> IO (CLong)
+
+cuddReadReorderingTime :: STDdManager s u -> ST s Int
+cuddReadReorderingTime = readIntegral c_cuddReadReorderingTime
+
+foreign import ccall safe "cudd.h Cudd_ReadReorderings"
+	c_cuddReadReorderings :: Ptr CDdManager -> IO (CUInt)
+
+cuddReadReorderings :: STDdManager s u -> ST s Int
+cuddReadReorderings = readIntegral c_cuddReadReorderings
+
+--Hooks
+foreign import ccall safe "cudd.h &Cudd_StdPreReordHook"
+	c_cuddStdPreReordHook :: HookFP
+
+foreign import ccall safe "cudd.h &Cudd_StdPostReordHook"
+	c_cuddStdPostReordHook :: HookFP
+
+foreign import ccall safe "cudd.h Cudd_EnableReorderingReporting"
+	c_cuddEnableReorderingReporting :: Ptr CDdManager -> IO (CInt)
+
+cuddEnableReorderingReporting :: STDdManager s u -> ST s Int
+cuddEnableReorderingReporting (STDdManager m) = unsafeIOToST $ liftM fromIntegral $ c_cuddEnableReorderingReporting m
+
+foreign import ccall safe "cudd.h Cudd_DisableReorderingReporting"
+	c_cuddDisableReorderingReporting :: Ptr CDdManager -> IO (CInt)
+
+cuddDisableReorderingReporting :: STDdManager s u -> ST s Int
+cuddDisableReorderingReporting (STDdManager m) = unsafeIOToST $ liftM fromIntegral $ c_cuddDisableReorderingReporting m
+
+foreign import ccall safe "cudd.h Cudd_ReorderingReporting"
+	c_cuddReorderingReporting :: Ptr CDdManager -> IO (CInt)
+
+cuddReorderingReporting :: STDdManager s u -> ST s Int
+cuddReorderingReporting (STDdManager m) = unsafeIOToST $ liftM fromIntegral $ c_cuddReorderingReporting m
+
+regStdPreReordHook :: STDdManager s u -> ST s Int
+regStdPreReordHook m = cuddAddHook m c_cuddStdPreReordHook CuddPreReorderingHook
+
+regStdPostReordHook :: STDdManager s u -> ST s Int
+regStdPostReordHook m = cuddAddHook m c_cuddStdPostReordHook CuddPostReorderingHook
+
+--Universal reordering params
+foreign import ccall safe "cudd.h Cudd_TurnOffCountDead"
+	c_cuddTurnOffCountDead :: Ptr CDdManager -> IO ()
+
+cuddTurnOffCountDead :: STDdManager s u -> ST s ()
+cuddTurnOffCountDead (STDdManager m) = unsafeIOToST $ c_cuddTurnOffCountDead m
+
+foreign import ccall safe "cudd.h Cudd_TurnOnCountDead"
+	c_cuddTurnOnCountDead :: Ptr CDdManager -> IO ()
+
+cuddTurnOnCountDead :: STDdManager s u -> ST s ()
+cuddTurnOnCountDead (STDdManager m) = unsafeIOToST $ c_cuddTurnOnCountDead m
+
+foreign import ccall safe "cudd.h Cudd_DeadAreCounted"
+	c_cuddDeadAreCounted :: Ptr CDdManager -> IO CInt
+
+cuddDeadAreCounted :: STDdManager s u -> ST s Int
+cuddDeadAreCounted (STDdManager m) = unsafeIOToST $ liftM fromIntegral $ c_cuddDeadAreCounted m
+
+--Sifting parameters
+foreign import ccall safe "cudd.h Cudd_ReadSiftMaxSwap"
+	c_cuddReadSiftMaxSwap :: Ptr CDdManager -> IO (CInt)
+
+cuddReadSiftMaxSwap :: STDdManager s u -> ST s Int
+cuddReadSiftMaxSwap = readIntegral c_cuddReadSiftMaxSwap
+
+foreign import ccall safe "cudd.h Cudd_SetSiftMaxSwap"
+	c_cuddSetSiftMaxSwap :: Ptr CDdManager -> CInt -> IO ()
+
+cuddSetSiftMaxSwap :: STDdManager s u -> Int -> ST s ()
+cuddSetSiftMaxSwap = setIntegral c_cuddSetSiftMaxSwap 
+
+foreign import ccall safe "cudd.h Cudd_ReadSiftMaxVar"
+	c_cuddReadSiftMaxVar :: Ptr CDdManager -> IO (Int)
+
+cuddReadSiftMaxVar :: STDdManager s u -> ST s Int
+cuddReadSiftMaxVar = readIntegral c_cuddReadSiftMaxVar
+
+foreign import ccall safe "cudd.h Cudd_SetSiftMaxVar"
+	c_cuddSetSiftMaxVar :: Ptr CDdManager -> CInt -> IO ()
+
+cuddSetSiftMaxVar :: STDdManager s u -> Int -> ST s ()
+cuddSetSiftMaxVar = setIntegral c_cuddSetSiftMaxVar
+	
+foreign import ccall safe "cudd.h Cudd_ReadNextReordering"
+	c_cuddReadNextReordering :: Ptr CDdManager -> IO (Int)
+
+cuddReadNextReordering :: STDdManager s u -> ST s Int
+cuddReadNextReordering = readIntegral c_cuddReadNextReordering
+
+foreign import ccall safe "cudd.h Cudd_SetNextReordering"
+	c_cuddSetNextReordering :: Ptr CDdManager -> CInt -> IO ()
+
+cuddSetNextReordering :: STDdManager s u -> Int -> ST s ()
+cuddSetNextReordering = setIntegral c_cuddSetNextReordering
+
+foreign import ccall safe "cudd.h Cudd_ReadMaxGrowthAlternate"
+	c_cuddReadMaxGrowthAlternate :: Ptr CDdManager -> IO CDouble
+
+cuddReadMaxGrowthAlternate :: STDdManager s u -> ST s Double
+cuddReadMaxGrowthAlternate = readFloat c_cuddReadMaxGrowthAlternate
+
+foreign import ccall safe "cudd.h Cudd_SetMaxGrowthAlternate"
+	c_cuddSetMaxGrowthAlternate :: Ptr CDdManager -> CDouble -> IO ()
+
+cuddSetMaxGrowthAlternate :: STDdManager s u -> Double -> ST s ()
+cuddSetMaxGrowthAlternate = setFloat c_cuddSetMaxGrowthAlternate
+
+foreign import ccall safe "cudd.h Cudd_ReadMaxGrowth"
+	c_cuddReadMaxGrowth :: Ptr CDdManager -> IO CDouble
+
+cuddReadMaxGrowth :: STDdManager s u -> ST s Double
+cuddReadMaxGrowth = readFloat c_cuddReadMaxGrowth
+
+foreign import ccall safe "cudd.h Cudd_SetMaxGrowth"
+	c_cuddSetMaxGrowth :: Ptr CDdManager -> CDouble -> IO ()
+
+cuddSetMaxGrowth :: STDdManager s u -> Double -> ST s ()
+cuddSetMaxGrowth = setFloat c_cuddSetMaxGrowth
+
+foreign import ccall safe "cudd.h Cudd_ReadReorderingCycle"
+	c_cuddReadReorderingCycle :: Ptr CDdManager -> IO (CInt)
+
+cuddReadReorderingCycle :: STDdManager s u -> ST s Int
+cuddReadReorderingCycle = readIntegral c_cuddReadReorderingCycle
+
+foreign import ccall safe "cudd.h Cudd_SetReorderingCycle"
+	c_cuddSetReorderingCycle :: Ptr CDdManager -> CInt -> IO ()
+
+cuddSetReorderingCycle :: STDdManager s u -> Int -> ST s ()
+cuddSetReorderingCycle = setIntegral c_cuddSetReorderingCycle
+
+--Genetic algorithm
+foreign import ccall safe "cudd.h Cudd_ReadPopulationSize"
+	c_cuddReadPopulationSize :: Ptr CDdManager -> IO (CInt)
+
+cuddReadPopulationSize :: STDdManager s u -> ST s Int
+cuddReadPopulationSize = readIntegral c_cuddReadPopulationSize
+
+foreign import ccall safe "cudd.h Cudd_SetPopulationSize"
+	c_cuddSetPopulationSize :: Ptr CDdManager -> CInt -> IO ()
+
+cuddSetPopulationSize :: STDdManager s u -> Int -> ST s ()
+cuddSetPopulationSize = setIntegral c_cuddSetPopulationSize
+
+foreign import ccall safe "cudd.h Cudd_ReadNumberXovers"
+	c_cuddReadNumberXovers :: Ptr CDdManager -> IO (CInt)
+
+cuddReadNumberXovers :: STDdManager s u -> ST s Int
+cuddReadNumberXovers = readIntegral c_cuddReadNumberXovers
+
+foreign import ccall safe "cudd.h Cudd_SetNumberXovers"
+	c_cuddSetNumberXovers :: Ptr CDdManager -> CInt -> IO ()
+
+cuddSetNumberXovers :: STDdManager s u -> Int -> ST s ()
+cuddSetNumberXovers = setIntegral c_cuddSetNumberXovers
+
+reordGCHook :: HookTyp
+reordGCHook _ _ _ = do
+    --putStrLn "reordGCHook"
+    performGC
+    --putStrLn "gc done"
+    return (fromIntegral 1)
+
+foreign import ccall "wrapper"
+    makeFunPtr :: HookTyp -> IO (FunPtr HookTyp)
+
+regReordGCHook :: STDdManager s u -> ST s Int
+regReordGCHook m = do
+    hk <- unsafeIOToST $ makeFunPtr reordGCHook
+    cuddAddHook m hk CuddPreReorderingHook
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/cudd.cabal b/cudd.cabal
new file mode 100644
index 0000000..9350ecc
--- /dev/null
+++ b/cudd.cabal
@@ -0,0 +1,71 @@
+name:                cudd
+version:             0.1.0.0
+synopsis:            Bindings to the CUDD binary decision diagrams library
+-- description:         
+license:             BSD3
+license-file:        LICENSE
+author:              Adam Walker
+maintainer:          adam.walker@nicta.com.au
+copyright:           2014 Adam Walker
+category:            Data
+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.Internal, 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:        . cudd dddmp epd mtr st util
+  cc-options:          -g -O3 -fpic -mtune=native -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
+  c-sources:           haskell_stubs/cuddwrap.c, haskell_stubs/stubs.c,
+                       cudd/cuddAPI.c, cudd/cuddAddAbs.c, cudd/cuddAddApply.c,
+                       cudd/cuddAddFind.c, cudd/cuddAddIte.c,
+                       cudd/cuddAddInv.c, cudd/cuddAddNeg.c,
+                       cudd/cuddAddWalsh.c, cudd/cuddAndAbs.c,
+                       cudd/cuddAnneal.c, cudd/cuddApa.c, cudd/cuddApprox.c,
+                       cudd/cuddBddAbs.c, cudd/cuddBddCorr.c,
+                       cudd/cuddBddIte.c, cudd/cuddBridge.c, cudd/cuddCache.c,
+                       cudd/cuddCheck.c, cudd/cuddClip.c, cudd/cuddCof.c,
+                       cudd/cuddCompose.c, cudd/cuddDecomp.c,
+                       cudd/cuddEssent.c, cudd/cuddExact.c, cudd/cuddExport.c,
+                       cudd/cuddGenCof.c, cudd/cuddGenetic.c,
+                       cudd/cuddGroup.c, cudd/cuddHarwell.c, cudd/cuddInit.c,
+                       cudd/cuddInteract.c, cudd/cuddLCache.c,
+                       cudd/cuddLevelQ.c, cudd/cuddLinear.c,
+                       cudd/cuddLiteral.c, cudd/cuddMatMult.c,
+                       cudd/cuddPriority.c, cudd/cuddRead.c, cudd/cuddRef.c,
+                       cudd/cuddReorder.c, cudd/cuddSat.c, cudd/cuddSign.c,
+                       cudd/cuddSolve.c, cudd/cuddSplit.c,
+                       cudd/cuddSubsetHB.c, cudd/cuddSubsetSP.c,
+                       cudd/cuddSymmetry.c, cudd/cuddTable.c, cudd/cuddUtil.c,
+                       cudd/cuddWindow.c, cudd/cuddZddCount.c,
+                       cudd/cuddZddFuncs.c, cudd/cuddZddGroup.c,
+                       cudd/cuddZddIsop.c, cudd/cuddZddLin.c,
+                       cudd/cuddZddMisc.c, cudd/cuddZddPort.c,
+                       cudd/cuddZddReord.c, cudd/cuddZddSetop.c,
+                       cudd/cuddZddSymm.c, cudd/cuddZddUtil.c,
+                       dddmp/dddmpStoreBdd.c, dddmp/dddmpStoreAdd.c,
+                       dddmp/dddmpStoreCnf.c, dddmp/dddmpLoad.c,
+                       dddmp/dddmpLoadCnf.c, dddmp/dddmpNodeBdd.c,
+                       dddmp/dddmpNodeAdd.c, dddmp/dddmpNodeCnf.c,
+                       dddmp/dddmpStoreMisc.c, dddmp/dddmpUtil.c,
+                       dddmp/dddmpBinary.c, dddmp/dddmpConvert.c,
+                       dddmp/dddmpDbg.c,
+                       epd/epd.c,
+                       mtr/mtrBasic.c, mtr/mtrGroup.c,
+                       st/st.c
+                       util/cpu_time.c, util/cpu_stats.c, util/safe_mem.c,
+                       util/strsav.c, util/texpand.c, util/ptime.c,
+                       util/prtime.c, util/pipefork.c, util/pathsearch.c,
+                       util/stub.c, util/datalimit.c
+  extra-libraries:     m
diff --git a/haskell_stubs/cuddwrap.c b/haskell_stubs/cuddwrap.c
new file mode 100644
index 0000000..04561c2
--- /dev/null
+++ b/haskell_stubs/cuddwrap.c
@@ -0,0 +1,116 @@
+#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;
+}
+
+void wrappedCuddDumpDot(DdManager *m, DdNode *f, char *filename){
+	printf("filename: %s\n", filename);
+	FILE *file = fopen(filename, "w");
+	assert(file);
+	Cudd_DumpDot(m, 1, &f, NULL, NULL, file);
+	fclose(file);
+}
+
+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/haskell_stubs/stubs.c b/haskell_stubs/stubs.c
new file mode 100644
index 0000000..32eeb06
--- /dev/null
+++ b/haskell_stubs/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;
+}
+