-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Bindings to the CUDD binary decision diagrams library -- -- Bindings to version 2.5.0 of the CUDD binary decision diagrams -- library. -- -- http://vlsi.colorado.edu/~fabio/CUDD/ -- -- Installation -- -- Either install CUDD using your system's package manager or download -- and build CUDD from here: https://github.com/adamwalker/cudd. -- This is a mirror of the CUDD source that has been modified to build -- shared object files. -- -- If you chose the latter option you need to tell cabal where to find -- cudd: -- -- "cabal install cudd --extra-include-dirs=/path/to/cudd/src/include -- --extra-lib-dirs=/path/to/cudd/src/libso" -- -- and you need to tell your program where to find the shared libraries: -- -- "LD_LIBRARY_PATH=/path/to/cudd/src/libso ghci" -- -- Usage -- -- This package provides two interfaces to the CUDD library: -- -- @package cudd @version 0.1.0.2 module Cudd.Common data SatBit [Zero] :: SatBit [One] :: SatBit [DontCare] :: SatBit toSatBit :: Int -> SatBit expand :: SatBit -> [Bool] cudd_unique_slots :: Int cudd_cache_slots :: Int instance Eq SatBit module Cudd.MTR newtype MtrNode s [MtrNode] :: (Ptr CMtrNode) -> MtrNode s data CMtrNode mtrAllocNode :: ST s (MtrNode s) mtrCreateFirstChild :: MtrNode s -> ST s (MtrNode s) mtrCreateLastChild :: MtrNode s -> ST s (MtrNode s) mtrDeallocNode :: MtrNode s -> ST s () mtrMakeFirstChild :: MtrNode s -> MtrNode s -> ST s () mtrMakeLastChild :: MtrNode s -> MtrNode s -> ST s () mtrMakeNextSibling :: MtrNode s -> MtrNode s -> ST s () mtrPrintGroups :: MtrNode s -> Int -> ST s () mtrPrintTree :: MtrNode s -> ST s () mtrMakeGroup :: MtrNode s -> Int -> Int -> Int -> ST s (MtrNode s) mtrInitGroupTree :: Int -> Int -> ST s (MtrNode s) mtrFindGroup :: MtrNode s -> Int -> Int -> ST s (MtrNode s) mtrDissolveGroup :: MtrNode s -> ST s () data MTRType [Mtrdefault] :: MTRType [Mtrterminal] :: MTRType [Mtrsoft] :: MTRType [Mtrfixed] :: MTRType [Mtrnewnode] :: MTRType instance Eq MTRType instance Show MTRType instance Enum MTRType module Cudd.C data CDDManager data CDDNode data CDDGen c_cuddReadOne :: Ptr CDDManager -> IO (Ptr CDDNode) c_cuddReadLogicZero :: Ptr CDDManager -> IO (Ptr CDDNode) c_cuddReadOneWithRef :: Ptr CDDManager -> IO (Ptr CDDNode) c_cuddReadLogicZeroWithRef :: Ptr CDDManager -> IO (Ptr CDDNode) c_cuddBddIthVar :: Ptr CDDManager -> CInt -> IO (Ptr CDDNode) c_cuddBddAnd :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddOr :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddNand :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddNor :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddXor :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddXnor :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddNot :: Ptr CDDNode -> IO (Ptr CDDNode) c_cuddNotNoRef :: Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddIte :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddExistAbstract :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddUnivAbstract :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddIterDerefBdd :: Ptr CDDManager -> Ptr CDDNode -> IO () cuddRef :: Ptr CDDNode -> IO () c_cuddInit :: CInt -> CInt -> CInt -> CInt -> CInt -> IO (Ptr CDDManager) c_cuddShuffleHeap :: Ptr CDDManager -> Ptr CInt -> IO CInt c_cuddSetVarMap :: Ptr CDDManager -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> CInt -> IO CInt c_cuddBddVarMap :: Ptr CDDManager -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddLeq :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO CInt c_cuddBddSwapVariables :: Ptr CDDManager -> Ptr CDDNode -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> CInt -> IO (Ptr CDDNode) c_cuddLargestCube :: Ptr CDDManager -> Ptr CDDNode -> Ptr CInt -> IO (Ptr CDDNode) c_cuddBddMakePrime :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddSupport :: Ptr CDDManager -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddSupportIndex :: Ptr CDDManager -> Ptr CDDNode -> IO (Ptr CInt) c_cuddSupportIndices :: Ptr CDDManager -> Ptr CDDNode -> Ptr (Ptr CInt) -> IO CInt c_cuddIndicesToCube :: Ptr CDDManager -> Ptr CInt -> CInt -> IO (Ptr CDDNode) c_cuddBddComputeCube :: Ptr CDDManager -> Ptr (Ptr CDDNode) -> Ptr CInt -> CInt -> IO (Ptr CDDNode) c_cuddBddToCubeArray :: Ptr CDDManager -> Ptr CDDNode -> Ptr CInt -> IO CInt c_cuddReadSize :: Ptr CDDManager -> IO CInt c_cuddBddCompose :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> CInt -> IO (Ptr CDDNode) c_cuddBddAndAbstract :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddXorExistAbstract :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddLeqUnless :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO CInt c_cuddEquivDC :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO CInt c_cuddXeqy :: Ptr CDDManager -> CInt -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> IO (Ptr CDDNode) c_cuddDebugCheck :: Ptr CDDManager -> IO CInt c_cuddCheckKeys :: Ptr CDDManager -> IO CInt c_cuddBddPickOneMinterm :: Ptr CDDManager -> Ptr CDDNode -> Ptr (Ptr CDDNode) -> CInt -> IO (Ptr CDDNode) c_cuddCheckZeroRef :: Ptr CDDManager -> IO CInt c_cuddReadInvPerm :: Ptr CDDManager -> CInt -> IO CInt c_cuddReadPerm :: Ptr CDDManager -> CInt -> IO CInt c_cuddDagSize :: Ptr CDDNode -> IO CInt c_cuddReadNodeCount :: Ptr CDDManager -> IO CLong c_cuddReadPeakNodeCount :: Ptr CDDManager -> IO CLong c_cuddReadMaxCache :: Ptr CDDManager -> IO CInt c_cuddReadMaxCacheHard :: Ptr CDDManager -> IO CInt c_cuddSetMaxCacheHard :: Ptr CDDManager -> CInt -> IO () c_cuddReadCacheSlots :: Ptr CDDManager -> IO CInt c_cuddReadCacheUsedSlots :: Ptr CDDManager -> IO CInt c_cuddBddAndLimit :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> CUInt -> IO (Ptr CDDNode) c_cuddBddNewVarAtLevel :: Ptr CDDManager -> CInt -> IO (Ptr CDDNode) c_cuddReadTree :: Ptr CDDManager -> IO (Ptr CMtrNode) c_cuddBddLICompaction :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddSqueeze :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddMinimize :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddEval :: Ptr CDDManager -> Ptr CDDNode -> Ptr CInt -> IO (Ptr CDDNode) c_cuddCountLeaves :: Ptr CDDNode -> IO CInt c_cuddCountMinterm :: Ptr CDDManager -> Ptr CDDNode -> CInt -> IO CDouble c_cuddCountPathsToNonZero :: Ptr CDDNode -> IO CDouble c_cuddCountPath :: Ptr CDDNode -> IO CDouble c_cuddBddConstrain :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddRestrict :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode) c_wrappedRegular :: Ptr CDDNode -> IO (Ptr CDDNode) c_cuddBddPermute :: Ptr CDDManager -> Ptr CDDNode -> Ptr CInt -> IO (Ptr CDDNode) c_cuddXgty :: Ptr CDDManager -> CInt -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> IO (Ptr CDDNode) c_cuddInequality :: Ptr CDDManager -> CInt -> CInt -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> IO (Ptr CDDNode) c_cuddDisequality :: Ptr CDDManager -> CInt -> CInt -> Ptr (Ptr CDDNode) -> Ptr (Ptr CDDNode) -> IO (Ptr CDDNode) c_cuddBddInterval :: Ptr CDDManager -> CInt -> Ptr (Ptr CDDNode) -> CInt -> CInt -> IO (Ptr CDDNode) c_cuddNodeReadIndex :: Ptr CDDNode -> IO CInt c_cuddBddTransfer :: Ptr CDDManager -> Ptr CDDManager -> Ptr CDDNode -> IO (Ptr CDDNode) c_cuddRecursiveDerefPtr :: FunPtr (Ptr CDDManager -> Ptr CDDNode -> IO ()) c_cuddDelayedDerefBddPtr :: FunPtr (Ptr CDDManager -> Ptr CDDNode -> IO ()) c_cuddIterDerefBddPtr :: FunPtr (Ptr CDDManager -> Ptr CDDNode -> IO ()) c_cuddBddNewVar :: Ptr CDDManager -> IO (Ptr CDDNode) c_cuddBddVectorCompose :: Ptr CDDManager -> Ptr CDDNode -> Ptr (Ptr CDDNode) -> IO (Ptr CDDNode) c_cuddQuit :: Ptr CDDManager -> IO () c_cuddPrintMinterm :: Ptr CDDManager -> Ptr CDDNode -> IO () c_cuddCheckCube :: Ptr CDDManager -> Ptr CDDNode -> IO CInt c_cuddPrintInfo :: Ptr CDDManager -> Ptr CFile -> IO CInt c_cuddPrintDebug :: Ptr CDDManager -> Ptr CDDNode -> CInt -> CInt -> IO CInt c_cuddIsComplement :: Ptr CDDNode -> CInt c_cuddDumpDot :: Ptr CDDManager -> CInt -> Ptr (Ptr CDDNode) -> Ptr CString -> Ptr CString -> Ptr CFile -> IO CInt c_cuddFirstCube :: Ptr CDDManager -> Ptr CDDNode -> Ptr (Ptr CInt) -> Ptr CInt -> IO (Ptr CDDGen) c_cuddNextCube :: Ptr CDDGen -> Ptr (Ptr CInt) -> Ptr CInt -> IO CInt c_cuddFirstPrime :: Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr (Ptr CInt) -> IO (Ptr CDDGen) c_cuddNextPrime :: Ptr CDDGen -> Ptr (Ptr CInt) -> IO CInt c_cuddIsGenEmpty :: Ptr CDDGen -> IO CInt c_cuddGenFree :: Ptr CDDGen -> IO CInt -- | An ST Monad based interface to the CUDD BDD library -- -- This is a straightforward wrapper around the C library. See -- http://vlsi.colorado.edu/~fabio/CUDD/ for documentation. -- -- Exampe usage: -- --
--   import Control.Monad.ST
--   import Cudd.Imperative
--   
--   main = do
--       res <- stToIO $ withManagerDefaults $ \manager -> do
--           v1      <- ithVar manager 0
--           v2      <- ithVar manager 1
--           conj    <- bAnd manager v1 v2
--           implies <- lEq manager conj v1
--           deref manager conj
--           return implies
--       print res
--   
module Cudd.Imperative newtype DDManager s u [DDManager] :: Ptr CDDManager -> DDManager s u [unDDManager] :: DDManager s u -> Ptr CDDManager newtype DDNode s u [DDNode] :: Ptr CDDNode -> DDNode s u [unDDNode] :: DDNode s u -> Ptr CDDNode cuddInit :: Int -> Int -> Int -> Int -> Int -> ST s (DDManager s u) cuddInitDefaults :: ST s (DDManager s u) withManager :: Int -> Int -> Int -> Int -> Int -> (forall u. DDManager s u -> ST s a) -> ST s a withManagerDefaults :: (forall u. DDManager s u -> ST s a) -> ST s a withManagerIO :: MonadIO m => Int -> Int -> Int -> Int -> Int -> (forall u. DDManager RealWorld u -> m a) -> m a withManagerIODefaults :: MonadIO m => (forall u. DDManager RealWorld u -> m a) -> m a shuffleHeap :: DDManager s u -> [Int] -> ST s () bZero :: DDManager s u -> DDNode s u bOne :: DDManager s u -> DDNode s u ithVar :: DDManager s u -> Int -> ST s (DDNode s u) bAnd :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) bOr :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) bNand :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) bNor :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) bXor :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) bXnor :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) bNot :: DDNode s u -> DDNode s u bIte :: DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) bExists :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) bForall :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) deref :: DDManager s u -> DDNode s u -> ST s () setVarMap :: DDManager s u -> [DDNode s u] -> [DDNode s u] -> ST s () varMap :: DDManager s u -> DDNode s u -> ST s (DDNode s u) lEq :: DDManager s u -> DDNode s u -> DDNode s u -> ST s Bool swapVariables :: DDManager s u -> [DDNode s u] -> [DDNode s u] -> DDNode s u -> ST s (DDNode s u) ref :: DDNode s u -> ST s () largestCube :: DDManager s u -> DDNode s u -> ST s (DDNode s u, Int) makePrime :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) support :: DDManager s u -> DDNode s u -> ST s (DDNode s u) supportIndices :: DDManager s u -> DDNode s u -> ST s [Int] indicesToCube :: DDManager s u -> [Int] -> ST s (DDNode s u) computeCube :: DDManager s u -> [DDNode s u] -> [Bool] -> ST s (DDNode s u) nodesToCube :: DDManager s u -> [DDNode s u] -> ST s (DDNode s u) readSize :: DDManager s u -> ST s Int bddToCubeArray :: DDManager s u -> DDNode s u -> ST s [SatBit] compose :: DDManager s u -> DDNode s u -> DDNode s u -> Int -> ST s (DDNode s u) andAbstract :: DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) xorExistAbstract :: DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) leqUnless :: DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s Bool equivDC :: DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s Bool xEqY :: DDManager s u -> [DDNode s u] -> [DDNode s u] -> ST s (DDNode s u) debugCheck :: DDManager s u -> ST s Int checkKeys :: DDManager s u -> ST s Int pickOneMinterm :: DDManager s u -> DDNode s u -> [DDNode s u] -> ST s (DDNode s u) toInt :: DDNode s u -> Int checkZeroRef :: DDManager s u -> ST s Int readInvPerm :: DDManager s u -> Int -> ST s Int readPerm :: DDManager s u -> Int -> ST s Int dagSize :: DDNode s u -> ST s Int readNodeCount :: DDManager s u -> ST s Integer readPeakNodeCount :: DDManager s u -> ST s Integer regular :: DDNode s u -> DDNode s u readMaxCache :: DDManager s u -> ST s Int readMaxCacheHard :: DDManager s u -> ST s Int setMaxCacheHard :: DDManager s u -> Int -> ST s () readCacheSlots :: DDManager s u -> ST s Int readCacheUsedSlots :: DDManager s u -> ST s Int cudd_unique_slots :: Int cudd_cache_slots :: Int andLimit :: DDManager s u -> DDNode s u -> DDNode s u -> Int -> ST s (Maybe (DDNode s u)) readTree :: DDManager s u -> ST s (MtrNode s) newVarAtLevel :: DDManager s u -> Int -> ST s (DDNode s u) liCompaction :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) squeeze :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) minimize :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u) newVar :: DDManager s u -> ST s (DDNode s u) vectorCompose :: DDManager s u -> DDNode s u -> [DDNode s u] -> ST s (DDNode s u) quit :: DDManager s u -> ST s () readIndex :: DDNode s u -> ST s Int printMinterm :: DDManager s u -> DDNode s u -> ST s () checkCube :: DDManager s u -> DDNode s u -> ST s Bool data Cube data Prime data DDGen s u t [DDGen] :: (Ptr CDDGen) -> DDGen s u t genFree :: DDGen s u t -> ST s () isGenEmpty :: DDGen s u t -> ST s Bool firstCube :: DDManager s u -> DDNode s u -> ST s (Maybe ([SatBit], DDGen s u Cube)) nextCube :: DDManager s u -> DDGen s u Cube -> ST s (Maybe [SatBit]) firstPrime :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (Maybe ([SatBit], DDGen s u Prime)) nextPrime :: DDManager s u -> DDGen s u Prime -> ST s (Maybe [SatBit]) instance Show (DDNode s u) instance Eq (DDNode s u) instance Ord (DDNode s u) module Cudd.Hook cuddAddHook :: DDManager s u -> HookFP -> CuddHookType -> ST s Int cuddRemoveHook :: DDManager s u -> HookFP -> CuddHookType -> ST s Int type HookTyp = Ptr CDDManager -> CString -> Ptr () -> IO (CInt) type HookFP = FunPtr HookTyp data CuddHookType [CuddPreGcHook] :: CuddHookType [CuddPostGcHook] :: CuddHookType [CuddPreReorderingHook] :: CuddHookType [CuddPostReorderingHook] :: CuddHookType instance Eq CuddHookType instance Show CuddHookType instance Enum CuddHookType module Cudd.Reorder data CuddReorderingType [CuddReorderSame] :: CuddReorderingType [CuddReorderNone] :: CuddReorderingType [CuddReorderRandom] :: CuddReorderingType [CuddReorderRandomPivot] :: CuddReorderingType [CuddReorderSift] :: CuddReorderingType [CuddReorderSiftConverge] :: CuddReorderingType [CuddReorderSymmSift] :: CuddReorderingType [CuddReorderSymmSiftConv] :: CuddReorderingType [CuddReorderWindow2] :: CuddReorderingType [CuddReorderWindow3] :: CuddReorderingType [CuddReorderWindow4] :: CuddReorderingType [CuddReorderWindow2Conv] :: CuddReorderingType [CuddReorderWindow3Conv] :: CuddReorderingType [CuddReorderWindow4Conv] :: CuddReorderingType [CuddReorderGroupSift] :: CuddReorderingType [CuddReorderGroupSiftConv] :: CuddReorderingType [CuddReorderAnnealing] :: CuddReorderingType [CuddReorderGenetic] :: CuddReorderingType [CuddReorderLinear] :: CuddReorderingType [CuddReorderLinearConverge] :: CuddReorderingType [CuddReorderLazySift] :: CuddReorderingType [CuddReorderExact] :: CuddReorderingType cuddReorderingStatus :: DDManager s u -> ST s (Int, CuddReorderingType) cuddAutodynEnable :: DDManager s u -> CuddReorderingType -> ST s () cuddAutodynDisable :: DDManager s u -> ST s () cuddReduceHeap :: DDManager s u -> CuddReorderingType -> Int -> ST s Int cuddMakeTreeNode :: DDManager s u -> Int -> Int -> Int -> ST s (Ptr ()) cuddReadReorderingTime :: DDManager s u -> ST s Int cuddReadReorderings :: DDManager s u -> ST s Int cuddEnableReorderingReporting :: DDManager s u -> ST s Int cuddDisableReorderingReporting :: DDManager s u -> ST s Int cuddReorderingReporting :: DDManager s u -> ST s Int regStdPreReordHook :: DDManager s u -> ST s Int regStdPostReordHook :: DDManager s u -> ST s Int cuddTurnOnCountDead :: DDManager s u -> ST s () cuddTurnOffCountDead :: DDManager s u -> ST s () cuddDeadAreCounted :: DDManager s u -> ST s Int cuddReadSiftMaxSwap :: DDManager s u -> ST s Int cuddSetSiftMaxSwap :: DDManager s u -> Int -> ST s () cuddReadSiftMaxVar :: DDManager s u -> ST s Int cuddSetSiftMaxVar :: DDManager s u -> Int -> ST s () cuddReadNextReordering :: DDManager s u -> ST s Int cuddSetNextReordering :: DDManager s u -> Int -> ST s () cuddReadMaxGrowthAlternate :: DDManager s u -> ST s Double cuddSetMaxGrowthAlternate :: DDManager s u -> Double -> ST s () cuddReadMaxGrowth :: DDManager s u -> ST s Double cuddReadReorderingCycle :: DDManager s u -> ST s Int cuddSetReorderingCycle :: DDManager s u -> Int -> ST s () cuddSetPopulationSize :: DDManager s u -> Int -> ST s () cuddReadNumberXovers :: DDManager s u -> ST s Int cuddSetNumberXovers :: DDManager s u -> Int -> ST s () regReordGCHook :: DDManager s u -> ST s Int instance Eq CuddReorderingType instance Show CuddReorderingType instance Enum CuddReorderingType module Cudd.GC cuddEnableGarbageCollection :: DDManager s u -> ST s () cuddDisableGarbageCollection :: DDManager s u -> ST s () cuddGarbageCollectionEnabled :: DDManager s u -> ST s Int c_preGCHook_sample :: HookFP c_postGCHook_sample :: HookFP regPreGCHook :: DDManager s u -> HookFP -> ST s Int regPostGCHook :: DDManager s u -> HookFP -> ST s Int -- | Bindings to the CUDD BDD library -- -- This is a straightforward wrapper around the C library. See -- http://vlsi.colorado.edu/~fabio/CUDD/ for documentation. -- -- Exampe usage: -- --
--   import Cudd.Cudd
--   
--   main = do
--       let manager = cuddInit
--           v1      = ithVar manager 0
--           v2      = ithVar manager 1
--           conj    = bAnd manager v1 v2
--           implies = lEq manager conj v1
--       print implies
--   
module Cudd.Cudd newtype DDManager [DDManager] :: (Ptr CDDManager) -> DDManager newtype DDNode [DDNode] :: ForeignPtr CDDNode -> DDNode [unDDNode] :: DDNode -> ForeignPtr CDDNode deref :: FunPtr (Ptr CDDManager -> Ptr CDDNode -> IO ()) cuddInit :: DDManager cuddInitOrder :: [Int] -> DDManager readOne :: DDManager -> DDNode readLogicZero :: DDManager -> DDNode ithVar :: DDManager -> Int -> DDNode bAnd :: DDManager -> DDNode -> DDNode -> DDNode bOr :: DDManager -> DDNode -> DDNode -> DDNode bNand :: DDManager -> DDNode -> DDNode -> DDNode bNor :: DDManager -> DDNode -> DDNode -> DDNode bXor :: DDManager -> DDNode -> DDNode -> DDNode bXnor :: DDManager -> DDNode -> DDNode -> DDNode bNot :: DDManager -> DDNode -> DDNode dumpDot' :: DDManager -> [DDNode] -> Maybe [String] -> Maybe [String] -> Ptr CFile -> IO Int dumpDot :: DDManager -> DDNode -> String -> IO Int cudd_cache_slots :: Int cudd_unique_slots :: Int eval :: DDManager -> DDNode -> [Int] -> Bool printMinterm :: DDManager -> DDNode -> IO () allSat :: DDManager -> DDNode -> [[SatBit]] oneSat :: DDManager -> DDNode -> Maybe [SatBit] onePrime :: DDManager -> DDNode -> DDNode -> Maybe [Int] supportIndex :: DDManager -> DDNode -> [Bool] bExists :: DDManager -> DDNode -> DDNode -> DDNode bForall :: DDManager -> DDNode -> DDNode -> DDNode bIte :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode permute :: DDManager -> DDNode -> [Int] -> DDNode swapVariables :: DDManager -> DDNode -> [DDNode] -> [DDNode] -> DDNode nodeReadIndex :: DDNode -> Int dagSize :: DDNode -> Int indicesToCube :: DDManager -> [Int] -> DDNode liCompaction :: DDManager -> DDNode -> DDNode -> DDNode minimize :: DDManager -> DDNode -> DDNode -> DDNode readSize :: DDManager -> Int xEqY :: DDManager -> [DDNode] -> [DDNode] -> DDNode xGtY :: DDManager -> [DDNode] -> [DDNode] -> DDNode interval :: DDManager -> [DDNode] -> Int -> Int -> DDNode disequality :: DDManager -> Int -> Int -> [DDNode] -> [DDNode] -> DDNode inequality :: DDManager -> Int -> Int -> [DDNode] -> [DDNode] -> DDNode ddNodeToInt :: Integral i => DDNode -> i pickOneMinterm :: DDManager -> DDNode -> [DDNode] -> Maybe DDNode readPerm :: DDManager -> Int -> Int readInvPerm :: DDManager -> Int -> Int readPerms :: DDManager -> [Int] readInvPerms :: DDManager -> [Int] readTree :: DDManager -> IO (Ptr CMtrNode) countLeaves :: DDNode -> Int countMinterm :: DDManager -> DDNode -> Int -> Double countPath :: DDNode -> Double countPathsToNonZero :: DDNode -> Double printDebug :: DDManager -> DDNode -> Int -> Int -> IO Int andAbstract :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode xorExistAbstract :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode transfer :: DDManager -> DDManager -> DDNode -> DDNode makePrime :: DDManager -> DDNode -> DDNode -> DDNode constrain :: DDManager -> DDNode -> DDNode -> DDNode restrict :: DDManager -> DDNode -> DDNode -> DDNode squeeze :: DDManager -> DDNode -> DDNode -> DDNode data SatBit [Zero] :: SatBit [One] :: SatBit [DontCare] :: SatBit largestCube :: DDManager -> DDNode -> (Int, DDNode) lEq :: DDManager -> DDNode -> DDNode -> Bool printInfo :: DDManager -> Ptr CFile -> IO Int instance Show DDNode instance Eq DDNode instance Ord DDNode module Cudd.Convert fromImperativeNode :: DDManager -> DDNode s u -> DDNode fromImperativeManager :: DDManager s u -> DDManager toImperativeNode :: DDNode -> ST s (DDNode s u) toImperativeManager :: DDManager -> DDManager s u module Cudd.File data DddmpVarInfoType [DddmpVarids] :: DddmpVarInfoType [DddmpVarpermids] :: DddmpVarInfoType [DddmpVarauxids] :: DddmpVarInfoType [DddmpVarnames] :: DddmpVarInfoType [DddmpVardefault] :: DddmpVarInfoType data DddmpMode [DddmpModeText] :: DddmpMode [DddmpModeBinary] :: DddmpMode [DddmpModeDefault] :: DddmpMode data DddmpVarMatchType [DddmpVarMatchids] :: DddmpVarMatchType [DddmpVarMatchpermids] :: DddmpVarMatchType [DddmpVarMatchauxids] :: DddmpVarMatchType [DddmpVarMatchnames] :: DddmpVarMatchType [DddmpVarComposeids] :: DddmpVarMatchType cuddBddStore :: DDManager -> String -> DDNode -> [Int] -> DddmpMode -> DddmpVarInfoType -> String -> IO Bool cuddBddLoad :: DDManager -> DddmpVarMatchType -> [Int] -> [Int] -> DddmpMode -> String -> IO (Maybe DDNode) instance Enum DddmpVarMatchType instance Enum DddmpVarInfoType instance Enum DddmpMode