-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Bindings to the CUDD binary decision diagrams library
--   
--   Bindings to version 3.0.0 of the CUDD binary decision diagrams
--   library.
--   
--   <a>http://vlsi.colorado.edu/~fabio/CUDD/</a>
--   
--   <i>Installation</i>
--   
--   Either install CUDD 3.0.0 using your system's package manager or
--   download and install CUDD from here:
--   <a>http://vlsi.colorado.edu/~fabio/</a>.
--   
--   Then:
--   
--   "cabal install cudd"
--   
--   Depending on where CUDD is installed on your system, you may need to
--   provide --extra-lib-dirs or --extra-include-dirs:
--   
--   "cabal install cudd --extra-lib-dirs=/usr/local/lib"
--   
--   <i>Usage</i>
--   
--   This package provides two interfaces to the CUDD library:
--   
--   <ul>
--   <li>A purely functional one in <a>Cudd.Cudd</a> that automatically
--   dereferences BDDs during garbage collection.</li>
--   <li>An ST Monad based one in <a>Cudd.Imperative</a> that gives you
--   precise control over the ordering of BDD operations and when BDDs are
--   dereferenced. Use this one if you want your code to perform well.</li>
--   </ul>
--   
--   Also, for a higher level interface in the style of the <a>ersatz</a>
--   SAT encoder, see <a>https://github.com/jwaldmann/cudd-ersatz/</a>.
@package cudd
@version 0.1.0.4

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 GHC.Classes.Eq Cudd.Common.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 GHC.Classes.Eq Cudd.MTR.MTRType
instance GHC.Show.Show Cudd.MTR.MTRType
instance GHC.Enum.Enum Cudd.MTR.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_cuddApaCountMinterm :: Ptr CDDManager -> Ptr CDDNode -> CInt -> Ptr CInt -> IO (Ptr CInt)
c_cuddFreeApaNumber :: Ptr CInt -> IO ()
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
c_cuddFirstNode :: Ptr CDDManager -> Ptr CDDNode -> Ptr (Ptr CDDNode) -> IO (Ptr CDDGen)
c_cuddNextNode :: Ptr CDDGen -> Ptr (Ptr CDDNode) -> IO CInt


-- | Bindings to the CUDD BDD library
--   
--   This is a straightforward wrapper around the C library. See
--   <a>http://vlsi.colorado.edu/~fabio/CUDD/</a> for documentation.
--   
--   Exampe usage:
--   
--   <pre>
--   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
--   </pre>
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 GHC.Show.Show Cudd.Cudd.DDNode
instance GHC.Classes.Eq Cudd.Cudd.DDNode
instance GHC.Classes.Ord Cudd.Cudd.DDNode


-- | An ST Monad based interface to the CUDD BDD library
--   
--   This is a straightforward wrapper around the C library. See
--   <a>http://vlsi.colorado.edu/~fabio/CUDD/</a> for documentation.
--   
--   Exampe usage:
--   
--   <pre>
--   import Control.Monad.ST
--   import Cudd.Imperative
--   
--   main = do
--       res &lt;- stToIO $ withManagerDefaults $ \manager -&gt; do
--           v1      &lt;- ithVar manager 0
--           v2      &lt;- ithVar manager 1
--           conj    &lt;- bAnd manager v1 v2
--           implies &lt;- lEq manager conj v1
--           deref manager conj
--           return implies
--       print res
--   </pre>
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 ()
countMintermExact :: DDManager s u -> DDNode s u -> Int -> ST s Integer
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])
firstNode :: DDManager s u -> DDNode s u -> ST s (Maybe (DDNode s u, DDGen s u Node))
nextNode :: DDManager s u -> DDGen s u Node -> ST s (Maybe (DDNode s u))
instance GHC.Show.Show (Cudd.Imperative.DDNode s u)
instance GHC.Classes.Eq (Cudd.Imperative.DDNode s u)
instance GHC.Classes.Ord (Cudd.Imperative.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 GHC.Classes.Eq Cudd.Hook.CuddHookType
instance GHC.Show.Show Cudd.Hook.CuddHookType
instance GHC.Enum.Enum Cudd.Hook.CuddHookType

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

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 GHC.Classes.Eq Cudd.Reorder.CuddReorderingType
instance GHC.Show.Show Cudd.Reorder.CuddReorderingType
instance GHC.Enum.Enum Cudd.Reorder.CuddReorderingType

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 GHC.Enum.Enum Cudd.File.DddmpVarMatchType
instance GHC.Enum.Enum Cudd.File.DddmpVarInfoType
instance GHC.Enum.Enum Cudd.File.DddmpMode