packages feed

cudd (empty) → 0.1.0.0

raw patch · 16 files changed

+2379/−0 lines, 16 filesdep +arraydep +basedep +mtlsetup-changed

Dependencies added: array, base, mtl, transformers

Files

+ Cudd/C.hs view
@@ -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+
+ Cudd/Common.hsc view
@@ -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+
+ Cudd/Convert.hs view
@@ -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
+ Cudd/Cudd.hs view
@@ -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 +
+ Cudd/File.chs view
@@ -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+
+ Cudd/ForeignHelpers.hs view
@@ -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+
+ Cudd/GC.hs view
@@ -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+
+ Cudd/Hook.chs view
@@ -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)
+ Cudd/Imperative.hs view
@@ -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+
+ Cudd/MTR.chs view
@@ -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) #}+
+ Cudd/Reorder.chs view
@@ -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+
+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ c_sources/cuddwrap.c view
@@ -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;+}+
+ c_sources/stubs.c view
@@ -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;+}+
+ cudd.cabal view
@@ -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