Safe Haskell	None
Language	Haskell2010

Cudd.Cudd

Description

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

Documentation

newtype DDManager Source

Constructors

DDManager (Ptr CDDManager)

newtype DDNode Source

Constructors

DDNode
Fields unDDNode :: ForeignPtr CDDNode

Instances

Eq DDNode
Ord DDNode
Show DDNode

deref :: FunPtr (Ptr CDDManager -> Ptr CDDNode -> IO ()) Source

cuddInit :: DDManager Source

cuddInitOrder :: [Int] -> DDManager Source

readOne :: DDManager -> DDNode Source

readLogicZero :: DDManager -> DDNode Source

ithVar :: DDManager -> Int -> DDNode Source

bAnd :: DDManager -> DDNode -> DDNode -> DDNode Source

bOr :: DDManager -> DDNode -> DDNode -> DDNode Source

bNand :: DDManager -> DDNode -> DDNode -> DDNode Source

bNor :: DDManager -> DDNode -> DDNode -> DDNode Source

bXor :: DDManager -> DDNode -> DDNode -> DDNode Source

bXnor :: DDManager -> DDNode -> DDNode -> DDNode Source

bNot :: DDManager -> DDNode -> DDNode Source

dumpDot' :: DDManager -> [DDNode] -> Maybe [String] -> Maybe [String] -> Ptr CFile -> IO Int Source

dumpDot :: DDManager -> DDNode -> String -> IO Int Source

cudd_cache_slots :: Int Source

cudd_unique_slots :: Int Source

eval :: DDManager -> DDNode -> [Int] -> Bool Source

printMinterm :: DDManager -> DDNode -> IO () Source

allSat :: DDManager -> DDNode -> [[SatBit]] Source

oneSat :: DDManager -> DDNode -> Maybe [SatBit] Source

onePrime :: DDManager -> DDNode -> DDNode -> Maybe [Int] Source

supportIndex :: DDManager -> DDNode -> [Bool] Source

bExists :: DDManager -> DDNode -> DDNode -> DDNode Source

bForall :: DDManager -> DDNode -> DDNode -> DDNode Source

bIte :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode Source

permute :: DDManager -> DDNode -> [Int] -> DDNode Source

swapVariables :: DDManager -> DDNode -> [DDNode] -> [DDNode] -> DDNode Source

nodeReadIndex :: DDNode -> Int Source

dagSize :: DDNode -> Int Source

indicesToCube :: DDManager -> [Int] -> DDNode Source

liCompaction :: DDManager -> DDNode -> DDNode -> DDNode Source

minimize :: DDManager -> DDNode -> DDNode -> DDNode Source

readSize :: DDManager -> Int Source

xEqY :: DDManager -> [DDNode] -> [DDNode] -> DDNode Source

xGtY :: DDManager -> [DDNode] -> [DDNode] -> DDNode Source

interval :: DDManager -> [DDNode] -> Int -> Int -> DDNode Source

disequality :: DDManager -> Int -> Int -> [DDNode] -> [DDNode] -> DDNode Source

inequality :: DDManager -> Int -> Int -> [DDNode] -> [DDNode] -> DDNode Source

ddNodeToInt :: Integral i => DDNode -> i Source

pickOneMinterm :: DDManager -> DDNode -> [DDNode] -> Maybe DDNode Source

readPerm :: DDManager -> Int -> Int Source

readInvPerm :: DDManager -> Int -> Int Source

readPerms :: DDManager -> [Int] Source

readInvPerms :: DDManager -> [Int] Source

readTree :: DDManager -> IO (Ptr CMtrNode) Source

countLeaves :: DDNode -> Int Source

countMinterm :: DDManager -> DDNode -> Int -> Double Source

countPath :: DDNode -> Double Source

countPathsToNonZero :: DDNode -> Double Source

printDebug :: DDManager -> DDNode -> Int -> Int -> IO Int Source

andAbstract :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode Source

xorExistAbstract :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode Source

transfer :: DDManager -> DDManager -> DDNode -> DDNode Source

makePrime :: DDManager -> DDNode -> DDNode -> DDNode Source

constrain :: DDManager -> DDNode -> DDNode -> DDNode Source

restrict :: DDManager -> DDNode -> DDNode -> DDNode Source

squeeze :: DDManager -> DDNode -> DDNode -> DDNode Source

data SatBit Source

Constructors

Zero
One
DontCare

Instances

Eq SatBit

largestCube :: DDManager -> DDNode -> (Int, DDNode) Source

lEq :: DDManager -> DDNode -> DDNode -> Bool Source

printInfo :: DDManager -> Ptr CFile -> IO Int Source