-- 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: -- --
-- 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